19 citations · 44 across the 8 of their papers we have counts for
9 papers
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…
Relative elegance and cartesian cubes with one connection
Evan Cavallo, Christian Sattler
We establish a Quillen equivalence between the Kan-Quillen model structure and a model structure, derived from a cubical model of homotopy type theory, on the category of cartesian…
Internalizing Representation Independence with Univalence
Carlo Angiuli, Evan Cavallo, Anders Mörtberg +1
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are rela…
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…
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…