Cubical Type Theory

Cyril Cohen, T. C., Huber, S., & Mörtberg, A. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.

Type

Preprint

Intellectual base

Grey literature

Link

https://arxiv.org/abs/1611.02108

Cited by

1 citation across 1 artifact.

Domain-specific

• Cubical Set
  • Awodey develops a cartesian cubical model of homotopy type theory, while Cohen, Coquand, Huber, and Mörtberg use a richer cubical model to give constructive computational meaning to univalence and to handle function extensionality and selected higher inductive types.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:4a4de123bc38 · see in the full table