Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our questions

5 votes
0 answers
204 views

Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination

0 votes
1 answer
127 views

Why inductive types (or variants) are so rigid in terms of the set of constructors

5 votes
2 answers
302 views

Type Theory Lean 3 to Lean 4

2 votes
1 answer
120 views

Provable `fun-ext`and "rewriting under binders" in intensional MLTT

0 votes
0 answers
97 views

Formalization of partial functions for combinatorial counting

4 votes
1 answer
94 views

General method for disproving possibility of judgemental equality

4 votes
1 answer
139 views

New types in higher order logic

1 vote
1 answer
20 views

Type class constaint is ignored in type synonym definition

2 votes
2 answers
134 views

What if identity type in extensional type theory were possibly non-deterministic?

4 votes
1 answer
168 views

Co-induction principle

2 votes
2 answers
231 views

Is there a most flexible type theory or proof assistant?

2 votes
1 answer
98 views

Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

2 votes
1 answer
81 views

Abstracting over large types in type theory

3 votes
2 answers
133 views

State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

Browse more Questions