Skip to main content
New
Stack Overflow Jobs powered by Indeed: A job site that puts thousands of tech jobs at your fingertips (U.S. only). Search jobs
ice1000's user avatar
ice1000's user avatar
ice1000's user avatar
ice1000
  • Member for 5 years, 7 months
  • Last seen more than a week ago
6 votes
Accepted

Example use cases for induction-recursion

5 votes

How does type theory change how one thinks about programming?

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

How to use Prop from UTT in Agda

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?

0 votes

Does the order of declarations in an inductive type matter?