Skip to main content

Explore our questions

7 votes
2 answers
543 views

Why do some people disagree about whether DTT implies not Turing complete?

1 vote
1 answer
462 views

Why does Agda use Set instead of Type?

3 votes
0 answers
125 views

Lower bounds in type theory proof assistant with ordinals and universes without axioms

11 votes
5 answers
2k views

How do real-world proof assistants bind variables and check equality?

26 votes
4 answers
2k views

What are the differences between MLTT and CIC?

6 votes
1 answer
109 views

What are the typechecking differences between records and iterated sigma types in Agda?

2 votes
2 answers
258 views

Has extensionality ever caused any problems in a mathematical proof?

3 votes
2 answers
269 views

How to convert Agda's with statement to a helper function?

2 votes
1 answer
64 views

Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?

3 votes
1 answer
402 views

How to provide proof for termination in Agda?

4 votes
2 answers
217 views

Binding variables to terms involving later variables

6 votes
1 answer
535 views

What are the principal differences between Agda's core type theory and Coq's?

3 votes
2 answers
161 views

Can Hyperreal exist a axiom-free implementation in HoTT?

7 votes
3 answers
1k views

How to run Agda?

Browse more Questions