On generalized algebraic theories and categories with families
From MaRDI portal
Publication:5084311
DOI10.1017/S0960129521000268MaRDI QIDQ5084311
Peter Dybjer, Martín Hötzel Escardó, Thierry Coquand, Marc Bezem
Publication date: 24 June 2022
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2012.08370
Martin-Löf type theorydependent type theoryinternal categoryinitial modelgeneralized algebraic theorycategory with families
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Partial Horn logic and Cartesian categories
- Generalized algebraic theories and contextual categories
- On functors expressible in the polymorphic typed lambda calculus
- Revisiting the categorical interpretation of dependent type theory
- Type theory in type theory using quotient inductive types
- Subsystems and regular quotients of C-systems
- The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
- Inductive-Inductive Definitions
- Extensional Constructs in Intensional Type Theory
- Internal type theory
- Conservativity of equality reflection over intensional type theory
- Categories with Families: Unityped, Simply Typed, and Dependently Typed
- Impredicative Encodings of (Higher) Inductive Types
- Large and Infinitary Quotient Inductive-Inductive Types
- The biequivalence of locally cartesian closed categories and Martin-Löf type theories
This page was built for publication: On generalized algebraic theories and categories with families
