Two-level type theory and applications
From MaRDI portal
Publication:6149950
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)
Abstract: We define and develop two-level type theory (2LTT), a version of Martin-L"of type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory. There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level $n$ can be constructed in HoTT for any externally fixed natural number $n$. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where $n$ will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models. Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky's Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be stated simply be asking the inner and outer natural numbers to be isomorphic. After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of (infinity,1)-category and give some examples.
Full work available at URL: https://arxiv.org/abs/1705.03307
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
Related Items (2)
Transpension: the right adjoint to the Pi-type ⋮ Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
This page was built for publication: Two-level type theory and applications
