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
2 votes

Derivability of `Vector` in pure calculus of constructions

5 votes
Accepted

Generalizations, or extensions of W-types in MLTT

9 votes

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

6 votes
Accepted

Dependent type theory and definitions of cumulativity

7 votes
Accepted

What is the computational power of the Calculus of Constructions?

20 votes
Accepted

Swapping arguments of variables in higher-order pattern unification

8 votes
Accepted

What's the categorical semantics of definitional equality?

6 votes

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

4 votes
Accepted

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

6 votes
Accepted

What technique is used to implement type checking for CoC?

7 votes
Accepted

Are uniqueness rules converse to introduction rules?

4 votes

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

6 votes

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

2 votes

Normal term of double negation of W-type

4 votes

Relating functors to relational functors with the parametricity translation

3 votes

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

9 votes

Semantic definition of strict positivity for a functor

4 votes

How to define list zipping categorically/inductively?

7 votes
Accepted

Structural equality of Pi Types with heterogeneous equality?

10 votes

Type-theoretic interpretation of Skolemization

8 votes
Accepted

Hereditary substitution with a universe hierarchy