23 citations · 34 across the 12 of their papers we have counts for
13 papers
Colimits in the -category of -topoi and étale morphisms
Taichi Uemura
We provide an alternative proof of Lurie's result that the wide subcategory of the -category of -topoi spanned by the étale morphisms is closed under small colimits…
An elementary definition of opetopic sets
Taichi Uemura
We propose elementary definitions of opetopes and opetopic sets. We directly define opetopic sets by a simple structure and several axioms. Opetopes are then opetopic sets satisfyi…
Higher inductive types in -categories
Taichi Uemura
We propose a definition of higher inductive types in -categories with finite limits. We show that the -category of -categories with higher induc…
Normalization and coherence for -type theories
Taichi Uemura
We develop a technique for normalization for -type theories. The normalization property helps us to prove a coherence theorem: the initial model of a given -type th…
Homotopy type theory as a language for diagrams of -logoses
Taichi Uemura
We show that certain diagrams of -logoses are reconstructed in homotopy type theory extended with some lex, accessible modalities, which enables us to use plain homotopy ty…
-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…
The Universal Exponentiable Arrow
Taichi Uemura
We show that the essentially algebraic theory of generalized algebraic theories, regarded as a category with finite limits, has a universal exponentiable arrow in the sense that an…
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…
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…
-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…
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…
Fibred Fibration Categories
Taichi Uemura
We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-Löf type theory. Fibred type-theoretic fibration categories…