Two-level type theory and applications
From MaRDI portal
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 can be constructed in HoTT for any externally fixed natural number . Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where 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.
Cites work
- A higher structure identity principle
- A minimalist two-level foundation for constructive mathematics
- A model for the homotopy theory of homotopy theory
- A type theory for synthetic -categories
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Extending homotopy type theory with strict equality
- Homotopy invariant algebraic structures on topological spaces
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Internal type theory
- Internal universes in models of homotopy type theory
- On higher inductive types in cubical type theory
- Partiality, Revisited
- Quasi-categories and Kan complexes
- Quasi-unital \(\infty\)-categories
- Quotient inductive-inductive types
- Signatures and induction principles for higher inductive-inductive types
- The general universal property of the propositional truncation
- The theory and practice of Reedy categories
- The univalence axiom for elegant Reedy presheaves
- Type theory in type theory using quotient inductive types
- Univalence for inverse diagrams and homotopy canonicity
Cited in
(7)- Transpension: the right adjoint to the Pi-type
- Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
- Second-order generalised algebraic theories: signatures and first-order semantics
- Formalizing two-level type theory with cofibrant exo-nat
- A parametricity-based formalization of semi-simplicial and semi-cubical sets
- Natural numbers from integers
- The univalence principle
This page was built for publication: Two-level type theory and applications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149950)
