Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our questions

2 votes
3 answers
75 views

Equality of records with members whose types are dependent (Lean 4)

5 votes
1 answer
194 views

Very dependent functions

10 votes
3 answers
121 views

Given `A = B`, how to prove `a: A` also has type B in Lean 4

1 vote
1 answer
105 views

Does Agda's --injective-type-constructors flag have canonicity?

4 votes
2 answers
146 views

Formalization of abstract definitions

2 votes
1 answer
122 views

What are references for learning type theory?

35 votes
3 answers
624 views

What is predicativity?

7 votes
0 answers
177 views

Alternatives to universe levels

13 votes
2 answers
421 views

What is a commuting conversion and why are they problematic?

3 votes
1 answer
105 views

What's the difference between a computation rule and a definitional equality?

6 votes
3 answers
436 views

How are the parts of category theory which make explicit reference to Set different when formalized in a proof assistant that is based on type theory

0 votes
0 answers
79 views

Existential variables in dependent type theory

5 votes
1 answer
248 views

What is a weak function space and what does it have to do with HOAS?

4 votes
2 answers
115 views

What is a non-canonical term?

Browse more Questions