Constructing a universe for the setoid model
From MaRDI portal
Publication:2233391
DOI10.1007/978-3-030-71995-1_1OpenAlexW3138716284MaRDI QIDQ2233391
Filippo Sestini, Christian Sattler, Ambrus Kaposi, Thorsten Altenkirch, Simon Boulier
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-71995-1_1
Related Items (1)
Cites Work
- Setoid type theory -- a syntactic translation
- Constructing a universe for the setoid model
- Type theory in type theory using quotient inductive types
- Positive Inductive-Recursive Definitions
- Constructing categories and setoids of setoids in type theory
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Internal type theory
- Conservativity of equality reflection over intensional type theory
- A Syntax for Higher Inductive-Inductive Types
- Small Induction Recursion
- Homotopy Type Theory: Univalent Foundations of Mathematics
- For Finitary Induction-Induction, Induction is Enough
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Constructing a universe for the setoid model
