User Konstantin Solomatov

41 votes

4 answers

8k views

Why does Coq have Prop?

asked Mar 31, 2014 at 3:13

21 votes

1 answer

2k views

Why it's impossible to declare an induction principle for Church numerals

asked Mar 25, 2015 at 21:53

11 votes

1 answer

1k views

Logical framework vs type theory

asked Feb 18, 2015 at 19:52

11 votes

1 answer

3k views

W-types vs Inductive types

asked Apr 17, 2014 at 6:07

10 votes

1 answer

373 views

Example of where violation of strict positivity condition in inductive types leads to inconsistency

asked Apr 1, 2014 at 22:09

8 votes

1 answer

776 views

Squash type vs Propositional truncation type

asked Feb 18, 2015 at 19:57

7 votes

1 answer

340 views

How Univalence can be used for proofs about algorithm correctness

asked Dec 23, 2014 at 19:34

7 votes

2 answers

694 views

"Correctness" of type theory

asked Apr 4, 2014 at 19:25

6 votes

1 answer

293 views

What does consistency mean for "computational theories" corresponding to inductive types?

asked Apr 17, 2014 at 17:22

6 votes

1 answer

779 views

Types which correspond to sets of cardinality of continuum

asked May 7, 2014 at 16:56

5 votes

3 answers

469 views

How to use Prop from UTT in Agda

asked Mar 30, 2014 at 21:50

5 votes

2 answers

609 views

Good description of Calculus of Inductive Construction

asked Mar 30, 2014 at 21:56

5 votes

3 answers

1k views

Law of excluded middle in MLTT

asked Dec 23, 2014 at 22:25

4 votes

0 answers

346 views

Category theory in plain MLTT

asked May 6, 2015 at 23:14

4 votes

2 answers

207 views

Well-formedness condition for inductive types

asked Mar 28, 2014 at 22:46

4 votes

1 answer

649 views

Rules about Prop and Set in UTT

asked May 11, 2014 at 6:18

4 votes

1 answer

2k views

Monomorphic vs Polymorphic type theory

asked Apr 30, 2014 at 20:03

Stack Exchange Network

17 Questions

Why does Coq have Prop?

Why it's impossible to declare an induction principle for Church numerals

Logical framework vs type theory

W-types vs Inductive types

Example of where violation of strict positivity condition in inductive types leads to inconsistency

Squash type vs Propositional truncation type

How Univalence can be used for proofs about algorithm correctness

"Correctness" of type theory

What does consistency mean for "computational theories" corresponding to inductive types?

Types which correspond to sets of cardinality of continuum

How to use Prop from UTT in Agda

Good description of Calculus of Inductive Construction

Law of excluded middle in MLTT

Category theory in plain MLTT

Well-formedness condition for inductive types

Rules about Prop and Set in UTT

Monomorphic vs Polymorphic type theory