23 citations · 34 across the 12 of their papers we have counts for
Showing 2019Show all
3 papers · 1 filter
math.LO2019
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…
math.CT2019★ 23 cited
A General Framework for the Semantics of Type Theory
Taichi Uemura
We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-Löf type theory, two-level type theory and cubical type theory. We e…
math.CT2019
-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.