Search

• < Previous
• 1
• Next >

---

Normalisation by Evaluation for Type Theory, in Type Theory

Thorsten Altenkirch ; Ambrus Kaposi.

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every&nbsp;[&hellip;]

---

Signatures and Induction Principles for Higher Inductive-Inductive Types

Ambrus Kaposi ; András Kovács.

Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher&nbsp;[&hellip;]

---