Proof Assistants Beta
Timo's user avatar
Timo's user avatar
Timo's user avatar
Timo
  • Member for 1 year
  • Last seen this week
  • Somewhere
Profile Activity
Stats
517
reputation
1k
reached
2
answers
8
questions
Communities
View all
About

Curious about metamathematics and computation

Badges
View all badges
This user doesn’t have any gold badges yet.
1
silver badge
10
bronze badges
Top tags
View all tags
6
Score
1
Posts
10
Posts %
1
Score
4
Posts
40
Posts %
1
Score
3
Posts
30
Posts %
1
Score
2
Posts
20
Posts %
0
Score
2
Posts
20
Posts %
0
Score
2
Posts
20
Posts %
Top posts
All Questions Answers
Score Newest
question
7
Can you build W-types out of natural numbers predicatively?
Aug 23, 2022
question
7
Proving strict positivity in Agda
Sep 28, 2022
answer
6
Does ST$\lambda$C equal to simple type theory?
May 28, 2022
question
5
What are the conditions for Agda to detect that induction-recursion has a least fixed point?
Oct 29, 2022
question
5
Proof-theoretic strength of HOL compared to predicative dependent types
Nov 1, 2022
question
5
State of art for observational equality, on the injectivity requirement
Feb 18
question
3
Uniform notions of pattern matching at dependent types with impredicative proof strength
Nov 9, 2022
answer
1
Proving strict positivity in Agda
Sep 30, 2022
question
1
Descriptions of heterogenous datatypes
Oct 13, 2022
question
0
Cardinals, universe levels, sheaves and predicativity
Jan 4
Top network posts
View all network posts
8
Type theory and fixed points of datatypes
8
Isbell duality between algebras and sheaves
7
Strongly normalizing type theory beyond induction-recursion
6
Programmatic higher inductive/inductive-inductive types with equalities between equalities
6
Are infinitary monads monadic?

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.