Indexed type theories

DOI10.1017/S0960129520000092MaRDI QIDQ5156767zbMATH OpenFDO

Authors Valery Isaev

Publication date 11 October 2021

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

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

zbMATH Keywords

category theoryhomotopy type theory

Mathematics Subject Classification ID

Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Abstract: In this paper, we define indexed type theories which are related to indexed ($infty$-)categories in the same way as (homotopy) type theories are related to ($infty$-)categories. We define several standard constructions for such theories including finite (co)limits, arbitrary (co)products, exponents, object classifiers, and orthogonal factorization systems. We also prove that these constructions are equivalent to their type theoretic counterparts such as $Sigma$-types, unit types, identity types, finite higher inductive types, $Pi$-types, univalent universes, and higher modalities.

Recommendations

• Categorical and algebraic aspects of Martin-Löf type theory
• The homotopy theory of type theories
• Model structures on categories of models of type theories
• A type theory for synthetic -categories
• Internal languages of finitely complete ( , 1)-categories

Cites work

• A type theory for synthetic -categories
• Adjoint functor theorems for -categories
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Fibrations of -categories
• Fibred fibration categories
• Generalizations of Hedberg's theorem
• Higher Topos Theory (AM-170)
• Homotopy limits in type theory
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3605078 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• Idempotents in intensional type theory
• Internal languages of finitely complete ( , 1)-categories
• Internal universes in models of homotopy type theory
• Invariance of the \(K\)-theory for derived equivalences
• Modalities in homotopy type theory
• On localization and stabilization for factorization systems
• Univalence in locally Cartesian closed categories

Cited in

(8)

• Search algorithms in type theory
• scientific article; zbMATH DE number 2090025 (Why is no real title available?)
• $L'$-localization in an $\infty$-topos
• Indexed containers
• 2-Dimensional Directed Type Theory
• Constructing coproducts in locally Cartesian closed -categories
• A formal logic for formal category theory
• Categorical and algebraic aspects of Martin-Löf type theory

This page was built for publication: Indexed type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5156767)