Searcharxiv⌕ Search

arXiv subjects

Taichi Uemura

Publications and source records attributed to Taichi Uemura.

13 recordsLinked to original sources
arXiv2026

Homotopy type theory as a language for diagrams of $\infty$-logoses

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 diagram of $\infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations.

math.CT↗
arXiv2025

Colimits in the $\infty$-category of $\infty$-topoi and étale morphisms

We provide an alternative proof of Lurie's result that the wide subcategory of the $\infty$-category of $\infty$-topoi spanned by the étale morphisms is closed under small colimits. Our proof is based on a new characterization of étale morphisms of $\infty$-topoi in relation to univalent families and does not rely on a larger universe. During the proof, we also give an elementary construction of univalent completion.

math.CT↗
arXiv2025

An elementary definition of opetopic sets

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 satisfying one more axiom. We show that our definition is equivalent to the polynomial monad definition given by Kock, Joyal, Batanin, and Mascari. We also show that our category of opetopes is equivalent to the one given by Ho Thanh.

math.CT↗
arXiv2024

Higher inductive types in $(\infty,1)$-categories

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 $(\infty,1)$-category with higher inductive types exists. We prove a form of canonicity: the global section functor for the initial $(\infty,1)$-category with higher inductive types preserves higher inductive types.

math.CT↗
arXiv2023

A General Framework for the Semantics of Type Theory

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 establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.

math.CT↗
arXiv2022

Normalization and coherence for $\infty$-type theories

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 ordinary type theory in $(\infty, 1)$-categorical structures.

math.LO↗
arXiv2022

$\infty$-type theories

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 initial models of $\infty$-type theories, the construction of internal languages of models of $\infty$-type theories, and the theory-model correspondence for $\infty$-type theories. Some structured $(\infty,1)$-categories are naturally regarded as models of some $\infty$-type theories. Thus, since every (1-categorical) type theory is in particular an $\infty$-type theory, $\infty$-type theories provide a unified framework for connections between type theories and $(\infty,1)$-categorical structures. As an application we prove Kapulkin and Lumsdaine's conjecture that the dependent type theory with intensional identity types gives internal languages for $(\infty,1)$-categories with finite limits.

math.CT↗
arXiv2021

The Universal Exponentiable Arrow

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 of the universal exponentiable arrow by an essentially unique functor.

math.CT↗
arXiv2019

On Church's Thesis in Cubical Assemblies

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 theory by constructing a reflective subuniverse of cubical assemblies where it holds.

math.LO↗
arXiv2019

$W$-Types in Categories of Coalgebras

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.

math.CT↗
arXiv2017

Fibred Fibration Categories

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 give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.

math.CT↗
arXiv2017

Homotopies for Free!

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 groups as some type of polymorphic functions defined without univalence or higher inductive types.

cs.LO↗