Univalent Semantics of Constructive Type Theories
No abstract available.
DOI 10.1007/978-3-642-25379-9_7
Related papers
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types JFP 2021
- Cubical agda: a dependently typed programming language with univalence and higher inductive types ICFP 2019
- Equivalences for free: univalent parametricity for effective transport ICFP 2018
- Computational higher-dimensional type theory POPL 2017
- HoTTSQL: proving query rewrites with univalent SQL semantics PLDI 2017
- Univalent higher categories via complete Semi-Segal types POPL 2018
- Computing Cohomology Rings in Cubical Agda CPP 2023
- Trocq: Proof Transfer for Free, With or Without Univalence ESOP 2024