Towards a directed homotopy type theory

DOI10.1016/J.ENTCS.2019.09.012MaRDI QIDQ2133175zbMATH OpenOpenAlexWikidataFDO

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

• 2-Dimensional Directed Type Theory
• Abstract homotopy theory and generalized sheaf cohomology
• Comprehension categories and the semantics of type dependency
• Homotopical algebra
• 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?)
• The identity type weak factorisation system
• The simplicial model of univalent foundations (after Voevodsky)

Cited in

(12)

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

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)