Towards a directed homotopy type theory

DOI10.1016/J.ENTCS.2019.09.012OpenAlexW2995356144WikidataQ113317351 ScholiaQ113317351MaRDI QIDQ2133175FDOQ2133175

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)

Cites Work

• Homotopical algebra
• Title not available (Why is that?)
• Title not available (Why is that?)
• The identity type weak factorisation system
• Comprehension categories and the semantics of type dependency
• Abstract homotopy theory and generalized sheaf cohomology
• Title not available (Why is that?)
• The simplicial model of univalent foundations (after Voevodsky)
• 2-Dimensional Directed Type Theory

Cited In (11)

• Transpension: the right adjoint to the Pi-type
• Bicategorical type theory: semantics and syntax
• Towards a directed homotopy type theory
• A formal logic for formal category theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Constructing higher inductive types as groupoid quotients
• Semantics for two-dimensional type theory
• Internal sums for synthetic fibered \((\infty,1)\)-categories
• 2-Dimensional Directed 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)