User András Kovács

20 votes

Accepted

Swapping arguments of variables in higher-order pattern unification

answered Dec 28, 2021 at 20:57

10 votes

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

answered Dec 22, 2023 at 19:57

10 votes

Type-theoretic interpretation of Skolemization

answered Aug 14, 2019 at 18:24

9 votes

Semantic definition of strict positivity for a functor

answered Feb 4, 2020 at 12:08

8 votes

Accepted

Hereditary substitution with a universe hierarchy

answered Nov 23, 2018 at 7:47

8 votes

Accepted

What's the categorical semantics of definitional equality?

answered Jul 28, 2021 at 11:40

7 votes

Accepted

Are uniqueness rules converse to introduction rules?

answered Apr 29, 2021 at 10:35

7 votes

Accepted

What is the computational power of the Calculus of Constructions?

answered Jun 8, 2022 at 6:06

7 votes

Accepted

Structural equality of Pi Types with heterogeneous equality?

answered Sep 30, 2019 at 23:20

6 votes

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

answered Mar 20, 2021 at 22:02

6 votes

Accepted

Dependent type theory and definitions of cumulativity

answered Oct 18, 2022 at 6:19

6 votes

Accepted

What technique is used to implement type checking for CoC?

answered May 16, 2021 at 9:43

6 votes

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

answered Jun 12, 2021 at 18:21

5 votes

Accepted

Generalizations, or extensions of W-types in MLTT

answered Jan 31 at 13:41

4 votes

Accepted

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

answered May 17, 2021 at 18:17

4 votes

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

answered Mar 28, 2021 at 13:50

4 votes

Relating functors to relational functors with the parametricity translation

answered Mar 15, 2021 at 7:46

4 votes

How to define list zipping categorically/inductively?

answered Dec 1, 2019 at 12:21

3 votes

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

answered Nov 30, 2020 at 10:47

2 votes

Normal term of double negation of W-type

answered Mar 19, 2021 at 6:47

2 votes

Derivability of `Vector` in pure calculus of constructions

answered Feb 4 at 14:49

Stack Exchange Network

21 Answers

Swapping arguments of variables in higher-order pattern unification

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

Type-theoretic interpretation of Skolemization

Semantic definition of strict positivity for a functor

Hereditary substitution with a universe hierarchy

What's the categorical semantics of definitional equality?

Are uniqueness rules converse to introduction rules?

What is the computational power of the Calculus of Constructions?

Structural equality of Pi Types with heterogeneous equality?

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

Dependent type theory and definitions of cumulativity

What technique is used to implement type checking for CoC?

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

Generalizations, or extensions of W-types in MLTT

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

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

Relating functors to relational functors with the parametricity translation

How to define list zipping categorically/inductively?

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

Normal term of double negation of W-type

Derivability of `Vector` in pure calculus of constructions