Weak omega-categories from intensional type theory

Types are weak omega-groupoids

We define a notion of weak omega-category internal to a model of Martin-Löf type theory, and prove that each type bears a canonical weak omega-category structure obtained from the tower of iterated identity types over that type. We show that the omega-categories arising in this way are in fact omega-groupoids.

Ω群的余代数模型

Coalgebraic models of Omega-groups

该研究在域上余交换余代数范畴中研究代数理论模型，建立相关范畴性质，引入带余交换Hopf代数结构的半阿贝尔范畴并将其刻画为Ω群代数理论的余代数模型。

$\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 $…

Martin-Löf Complexes

In this paper we define Martin-Löf complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-Löf type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-Löf complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-Löf complexes are a model of homotopy 1-types.

单值基础中类型论的范畴结构

Categorical structures for type theory in univalent foundations

本文在单值类型论中比较三种依赖类型论模型结构，构造映射并证明在单值公理下部分等价，引入相对宇宙研究其沿范畴等价及Rezk完备化的转移，并在Coq/UniMath中形式化。

Constructing categories and setoids of setoids in type theory

In this paper we consider the problem of building rich categories of setoids, in standard intensional Martin-Löf type theory (MLTT), and in particular how to handle the problem of equality on objects in this context. Any (proof-irrelevant) family F of setoids over a setoid A gives rise to a category C(A, F) of setoids with objects A. We may regard the family F as a setoid of setoids, and a crucial issue in this article is to construct rich or large enough such families. Depending on closure conditions of F, the category C(A, F) has corresponding categorical constructions. We exemplify this wit…

Separating Path and Identity Types in Presheaf Models of Univalent Type Theory

We give a collection of results regarding path types, identity types and univalent universes in certain models of type theory based on presheaves. The main result is that path types cannot be used directly as identity types in any Orton-Pitts style model of univalent type theory with propositional truncation in presheaf assemblies over the first and second Kleene algebras. We also give a Brouwerian counterexample showing that there is no constructive proof that there is an Orton-Pitts model of type theory in presheaves when the universe is based on a standard construction due to Hofmann and St…