On generalized algebraic theories and categories with families

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

zbMATH Keywords

Martin-Löf type theorydependent type theoryinternal categoryinitial modelgeneralized algebraic theorycategory with families

Mathematics Subject Classification ID

Type theory (03B38)

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