Search

• < Previous
• 1
• Next >

---

Proof-irrelevant model of CC with predicative induction and judgmental equality

Gyesik Lee ; Benjamin Werner.

We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace encoding which is universally defined for any function&nbsp;[&hellip;]

---

On the strength of proof-irrelevant type theories

Benjamin Werner.

We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. We show that in these&nbsp;[&hellip;]

---