Zobrazeno 1 - 10
of 40
pro vyhledávání: '"Uemura, Taichi"'
Autor:
Uemura, Taichi
We propose a definition of higher inductive types in $(\infty,1)$-categories with finite limits. We show that the $(\infty,1)$-category of $(\infty,1)$-categories with higher inductive types is finitarily presentable. In particular, the initial $(\in
Externí odkaz:
http://arxiv.org/abs/2410.17615
Autor:
Uemura, Taichi
We develop a technique for normalization for $\infty$-type theories. The normalization property helps us to prove a coherence theorem: the initial model of a given $\infty$-type theory is $0$-truncated. The coherence theorem justifies interpreting an
Externí odkaz:
http://arxiv.org/abs/2212.11764
Autor:
Uemura, Taichi
We show that certain diagrams of $\infty$-logoses are reconstructed in homotopy type theory extended with some lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $\infty$-logos but also a
Externí odkaz:
http://arxiv.org/abs/2212.02444
Autor:
Nguyen, Hoang Kim, Uemura, Taichi
We introduce $\infty$-type theories as an $\infty$-categorical generalization of the categorical definition of type theories introduced by the second named author. We establish analogous results to the previous work including the construction of init
Externí odkaz:
http://arxiv.org/abs/2205.00798
Autor:
Uemura, Taichi
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 any exponentiable arrow in any category with finite limits is the image
Externí odkaz:
http://arxiv.org/abs/2001.09940
Autor:
Swan, Andrew, Uemura, Taichi
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 that nevertheless Church's thesis is consistent with univalent type theor
Externí odkaz:
http://arxiv.org/abs/1905.03014
Autor:
Uemura, Taichi
We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-L\"{o}f type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory: every type
Externí odkaz:
http://arxiv.org/abs/1904.04097
Autor:
Uemura, Taichi
We construct $W$-types in the category of coalgebras for a cartesian comonad. It generalizes the constructions of $W$-types in presheaf toposes and gluing toposes.
Externí odkaz:
http://arxiv.org/abs/1901.06539
Autor:
Uemura, Taichi
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 assembly model does not satisfy a form of propositional resizing.
Externí odkaz:
http://arxiv.org/abs/1803.06649
Autor:
Uemura, Taichi
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 every space defined as a higher inductive type has the same homotopy group
Externí odkaz:
http://arxiv.org/abs/1701.07937