3 papers
math.CT2019
Stable factorization from a fibred algebraic weak factorization system
Evan Cavallo
We present a construction of stable diagonal factorizations, used to define categorical models of type theory with identity types, from a family of algebraic weak factorization sys…
cs.LO2019
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…
cs.LO2018
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…