19 citations · 44 across the 8 of their papers we have counts for
6 papers · 1 filter
Univalence without function extensionality
Evan Cavallo, Jonas Höfer
It is a well-known theorem of homotopy type theory, originally due to Voevodsky, that function extensionality holds inside any univalent universe. We consider a weaker variant of t…
Automating Boundary Filling in Cubical Type Theories
Maximilian Doré, Evan Cavallo, Anders Mörtberg
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to rea…
Internal Parametricity for Cubical Type Theory
Evan Cavallo, Robert Harper
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory suppo…
Parametric Cubical Type Theory
Evan Cavallo, Robert Harper
We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric typ…
The RedPRL Proof Assistant (Invited Paper)
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou +2
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type the…
Computational Higher Type Theory IV: Inductive Types
Evan Cavallo, Robert Harper
This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define…