A Constructive Model of Directed Univalence in Bicubical Sets
DOI10.1145/3373718.3394794zbMATH Open1498.03038OpenAlexW3031494424MaRDI QIDQ5145691FDOQ5145691
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
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
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)
Cited In (12)
- Transpension: the right adjoint to the Pi-type
- Title not available (Why is that?)
- Bicategorical type theory: semantics and syntax
- Bicategories in univalent foundations
- 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
- Semantics for two-dimensional type theory
- Internal sums for synthetic fibered \((\infty,1)\)-categories
- Constructive sheaf models of 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)
