Internal universes in models of homotopy type theory

DOI10.4230/LIPICS.FSCD.2018.22MaRDI QIDQ4993352zbMATH OpenFDO

Authors Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters

Publication date 15 June 2021

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

zbMATH Keywords

cubical setsdependent type theoryhomotopy type theoryinternal languagemodalitiesunivalent foundationsuniverses

Mathematics Subject Classification ID

Type theory (03B38) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Recommendations

• Axioms for modelling cubical type theory in a topos
• scientific article; zbMATH DE number 7003193
• Modalities in homotopy type theory
• Univalence for inverse diagrams and homotopy canonicity
• Natural models of homotopy type theory

Cites work

• A judgmental reconstruction of modal logic
• Axiomatic cohesion
• Contextual modal type theory
• Corrections to ``On right adjoints to exponential functors
• Cubical type theory: a constructive interpretation of the univalence axiom
• Fibrational modal type theory
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 3739803 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1420782 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Internal type theory
• The Frobenius condition, right properness, and uniform fibrations
• Varieties of cubical sets

Cited in

(31)

• Semantical analysis of contextual types
• scientific article; zbMATH DE number 7003193 (Why is no real title available?)
• Models of type theory based on Moore paths
• Model structures on categories of models of type theories
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Model structure on the universe of all types in interval type theory
• Syntax and models of Cartesian cubical type theory
• Canonicity and homotopy canonicity for cubical type theory
• Cubical methods in homotopy type theory and univalent foundations
• On Church’s thesis in cubical assemblies
• A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
• Homotopy canonicity for cubical type theory
• Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
• Dual-context calculi for modal logic
• Multimodal dependent type theory
• Indexed type theories
• Modal dependent type theory and dependent right adjoints
• Axioms for modelling cubical type theory in a topos
• Normalization by evaluation for modal dependent type theory
• A general framework for the semantics of type theory
• Two-level type theory and applications
• Constructing initial algebras using inflationary iteration
• Transpension: the right adjoint to the Pi-type
• Kripke-Joyal forcing for type theory and uniform fibrations
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• A categorical normalization proof for the modal lambda-calculus
• Homotopy type theory as a language for diagrams of -logoses
• Displayed type theory and semi-simplicial types
• Unifying cubical and multimodal type theory
• The equivariant model structure on cartesian cubical sets
• Separating path and identity types in presheaf models of univalent type theory

Describes a project that uses

Uses Software

• cart-cube
• cubicaltt
• GitHub

This page was built for publication: Internal universes in models of homotopy type theory

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