Skip to main content

Explore our questions

3 votes
1 answer
288 views

Why does `#check add_mul (R := ℕ)` return `add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b *` instead of `add_mul : Prop`?

26 votes
4 answers
1k views

What are the differences between MLTT and CIC?

4 votes
2 answers
131 views

Parametricity and data kinds

11 votes
3 answers
663 views

Given `A = B`, how to prove `a: A` also has type B in Lean 4

1 vote
0 answers
103 views

Proving Quine's notion that identity belongs to logic within type-constrained proof assistants

2 votes
2 answers
148 views

How exactly solved metas "revisited" in an efficient dependent type checker?

3 votes
1 answer
184 views

What is the well-established η law for naturals?

3 votes
1 answer
147 views

What are deductive systems associated with raw type theories?

1 vote
3 answers
129 views

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

0 votes
0 answers
118 views

MLTT with first-order reasoning and equality-reasoning information preservation

3 votes
1 answer
152 views

Does equality in $\Sigma_{(x : X)} x = x$ implies UIP?

4 votes
0 answers
120 views

Proving "proof methods" as theorems in type-theory based proof systems

2 votes
1 answer
167 views

Are type universes related to proper classes from set theory?

3 votes
0 answers
91 views

Limitations of simple type theory proof assistants for undergraduate-level mathematics?

Browse more Questions