Showing cs.LOShow all
2 papers · 1 filter
cs.LO2018
Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
Taichi Uemura
We construct a model of cubical type theory with a univalent and impredicative universe in a category of cubical assemblies. We show that this impredicative universe in the cubical…
cs.LO2017
Homotopies for Free!
Taichi Uemura
We show "free theorems" in the style of Wadler for polymorphic functions in homotopy type theory as consequences of the abstraction theorem. As an application, it follows that ever…