Two-level type theory and applications

DOI10.1017/S0960129523000130arXiv1705.03307OpenAlexW4380538482MaRDI QIDQ6149950

Christian Sattler, Nicolai Kraus, Paolo Capriotti, Danil Annenkov

Publication date: 5 March 2024

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1705.03307

zbMATH Keywords

homotopy type theoryconservativityhigher categorytwo-level type theoryhomotopy type system2LTT

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quasi-unital \(\infty\)-categories
• A minimalist two-level foundation for constructive mathematics
• Quotient inductive-inductive types
• Homotopy invariant algebraic structures on topological spaces
• Quasi-categories and Kan complexes
• Type theory in type theory using quotient inductive types
• The theory and practice of Reedy categories
• Partiality, Revisited
• A type theory for synthetic $\infty$-categories
• A model for the homotopy theory of homotopy theory
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Internal type theory
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• On Higher Inductive Types in Cubical Type Theory
• A Higher Structure Identity Principle
• The General Universal Property of the Propositional Truncation
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves

This page was built for publication: Two-level type theory and applications