user avatar
user avatar
user avatar
ice1000
  • Member for 3 years, 10 months
  • Last seen more than a week ago
5 votes

How does type theory change how one thinks about programming?

4 votes
Accepted

Example use cases for induction-recursion

4 votes
Accepted

How to think about `comp` in cubical type theory

3 votes
Accepted

Counterexample request: ill-scoped metavariable solution

3 votes
Accepted

NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?

2 votes

How does axiom K contradict univalence?

2 votes

What is the point of the eliminator for the unit type?

2 votes

Pi-type over a list in dependent type theory

2 votes

Does univ : univ always lead to a contradiction in a dependently typed language?

2 votes
Accepted

References on implementing universe levels over MLTT?

2 votes
Accepted

Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?

1 vote

What technique is used to implement type checking for CoC?

1 vote

How to use Prop from UTT in Agda

0 votes

Does the order of declarations in an inductive type matter?