4 papers
-type theories
Hoang Kim Nguyen, Taichi Uemura
We introduce -type theories as an -categorical generalization of the categorical definition of type theories introduced by the second named author. We establish ana…
On Church's Thesis in Cubical Assemblies
Andrew Swan, Taichi Uemura
We show that Church's thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We show tha…
-Types in Categories of Coalgebras
Taichi Uemura
We construct -types in the category of coalgebras for a cartesian comonad. It generalizes the constructions of -types in presheaf toposes and gluing toposes.
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…