Skip to main content
Share Your Experience: Take the 2024 Developer Survey
András Kovács's user avatar
András Kovács's user avatar
András Kovács's user avatar
András Kovács
  • Member for 10 years, 1 month
  • Last seen more than a month ago
20 votes
Accepted

Swapping arguments of variables in higher-order pattern unification

10 votes

Type-theoretic interpretation of Skolemization

9 votes

Semantic definition of strict positivity for a functor

9 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

8 votes
Accepted

Hereditary substitution with a universe hierarchy

8 votes
Accepted

What's the categorical semantics of definitional equality?

7 votes
Accepted

Are uniqueness rules converse to introduction rules?

7 votes
Accepted

What is the computational power of the Calculus of Constructions?

7 votes
Accepted

Structural equality of Pi Types with heterogeneous equality?

6 votes

Model of MLTT with $\eta$ rule where function extensionality fails

6 votes
Accepted

Dependent type theory and definitions of cumulativity

6 votes
Accepted

What technique is used to implement type checking for CoC?

6 votes

External failure of law of excluded middle in Martin-Löf type theory

5 votes
Accepted

Generalizations, or extensions of W-types in MLTT

4 votes
Accepted

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

4 votes

Dependent eliminator for empty type in intensional Martin-Löf type theory

4 votes

Relating functors to relational functors with the parametricity translation

4 votes

How to define list zipping categorically/inductively?

3 votes

Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

2 votes

Normal term of double negation of W-type

2 votes

Derivability of `Vector` in pure calculus of constructions