Towards a directed homotopy type theory

DOI10.1016/J.ENTCS.2019.09.012MaRDI QIDQ2133175OpenAlexWikidataFDO

Authors Paige Randall North

Publication date 29 April 2022

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

zbMATH Keywords

dependent type theorydirected homotopy theorysemantics of type theory

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• 2-Dimensional Directed Type Theory
• Path categories and propositional identity types
• A Constructive Model of Directed Univalence in Bicubical Sets
• Type theory and homotopy
• Topological and simplicial models of identity types

Cites work

• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• 2-Dimensional Directed Type Theory
• Abstract homotopy theory and generalized sheaf cohomology
• Comprehension categories and the semantics of type dependency
• Homotopical algebra
• The identity type weak factorisation system
• The simplicial model of univalent foundations (after Voevodsky)

Cited in

(11)

• Bicategorical type theory: semantics and syntax
• A formal logic for formal category theory
• Constructing higher inductive types as groupoid quotients
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Towards a directed homotopy type theory
• Internal sums for synthetic fibered \((\infty,1)\)-categories
• Semantics for two-dimensional type theory
• 2-Dimensional Directed Type Theory
• Transpension: the right adjoint to the Pi-type
• Synthetic fibered \((\infty,1)\)-category theory
• From cubes to twisted cubes via graph morphisms in type theory

This page was built for publication: Towards a directed homotopy type theory

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