
Internalizing Representation Independence with Univalence
In their usual form, representation independence metatheorems provide an...
read it

Internal Parametricity for Cubical Type Theory
We define a computational type theory combining the contentful equality ...
read it

Stable factorization from a fibred algebraic weak factorization system
We present a construction of stable diagonal factorizations, used to def...
read it

Parametric Cubical Type Theory
We exhibit a computational type theory which combines the higherdimensi...
read it

The RedPRL Proof Assistant (Invited Paper)
RedPRL is an experimental proof assistant based on Cartesian cubical com...
read it

Computational Higher Type Theory IV: Inductive Types
This is the fourth in a series of papers extending MartinLöf's meaning ...
read it
Evan Cavallo
is this you? claim profile