A Constructive Model of Directed Univalence in Bicubical Sets

DOI10.1145/3373718.3394794MaRDI QIDQ5145691zbMATH OpenOpenAlexFDO

Authors Matthew Z. Weaver, Daniel R. Licata

Publication date 21 January 2021

Published in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3373718.3394794

zbMATH Keywords

homotopy type theorydirected type theorydirected univalence

Mathematics Subject Classification ID

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

Recommendations

• The univalence axiom in cubical sets
• Towards a constructive simplicial model of Univalent Foundations
• Directoids: Algebraic models of up-directed sets
• scientific article; zbMATH DE number 1817702
• On the construction of uninorms on bounded lattices
• On univoque and strongly univoque sets
• Directed Sets and Malitz‐Cauchy‐Completions
• Undirected replicas of directional binary algebras.
• A class of uniform amarts indexed by directed sets
• Constructive models of uncountably categorical theories

Cited in

(13)

• Transpension: the right adjoint to the Pi-type
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Bicategorical type theory: semantics and syntax
• Bicategories in univalent foundations
• A formal logic for formal category theory
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Semantics for two-dimensional type theory
• Internal sums for synthetic fibered \((\infty,1)\)-categories
• Synthetic fibered \((\infty,1)\)-category theory
• Internal parametricity for cubical type theory
• Constructive sheaf models of type theory
• From cubes to twisted cubes via graph morphisms in type theory
• Syntax and models of Cartesian cubical type theory

This page was built for publication: A Constructive Model of Directed Univalence in Bicubical Sets

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