A Constructive Model of Directed Univalence in Bicubical Sets

DOI10.1145/3373718.3394794zbMath1498.03038OpenAlexW3031494424MaRDI QIDQ5145691

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

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

Related Items (7)

Constructive sheaf models of type theory ⋮ A formal logic for formal category theory ⋮ Bicategorical type theory: semantics and syntax ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Syntax and models of Cartesian cubical type theory

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