scientific article; zbMATH DE number 7761009

DOI10.4230/LIPICS.TYPES.2017.6zbMath1528.03110arXiv1712.04890MaRDI QIDQ6060677

Ian Orton, Andrew M. Pitts

Publication date: 3 November 2023

Full work available at URL: https://arxiv.org/abs/1712.04890

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

univalencehomotopy type theorydependent type theorycubical setsunivalent type theorycubical type theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Homotopical algebra, Quillen model categories, derivators (18N40) Type theory (03B38)

Related Items (1)

Univalent polymorphism

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Internal type theory
• Guarded Cubical Type Theory: Path Equality for Guarded Recursion
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: