The univalence axiom in posetal model categories

The univalence axiom for elegant Reedy presheaves

We show that Voevodsky's univalence axiom for intensional type theory is valid in categories of simplicial presheaves on elegant Reedy categories. In addition to diagrams on inverse categories, as considered in previous work of the author, this includes bisimplicial sets and $Θ_n$-spaces. This has potential applications to the study of homotopical models for higher categories.

External univalence for second-order generalized algebraic theories

Voevodsky's univalence axiom is often motivated as a realization of the equivalence principle; the idea that equivalent mathematical structures satisfy the same properties. Indeed, in Homotopy Type Theory, properties and structures can be transported over type equivalences. However, we may wish to explain the equivalence principle without relying on the univalence axiom. For example, all type formers preserve equivalences in most type theories; thus it should be possible to transport structures over type equivalences even in non-univalent type theories. We define external univalence, a propert…

On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom

In this article the author endows the functor category [B(C2),Gpd] with the structure of a type-theoretic fibration category with a universe using the projective fibrations. It offers a new model of Martin-Löf type theory with dependent sums, dependent products, identity types and a universe. It turns out that this universe, the natural candidate that lifts the univalent universe of small discrete groupoids in the groupoid model of Hofmann and Streicher, is not univalent.

(指向性) 在类型理论宇宙范畴模型中的合一性

(Pointed) Univalence in Universe Category Models of Type Theory

本文在类型理论宇宙范畴模型中提出指向性合一公理，结合计算与语义特性，验证其在同调理论中的封闭性。

On lifting univalence to the equivariant setting

This PhD thesis deals with some new models of intensional type theory and the Univalence Axiom introduced by Vladimir Voevodsky. Our work takes place in the framework of the definitions of type-theoretic fibration categories (the notion of model under consideration in this thesis) and universe in a type-theoretic fibration category, definitions due to Michael Shulman. The goal of this thesis consists mainly in the exploration of the stability of the univalence axiom, in particular in the following sense: being given a type-theoretic fibration category C equipped with a univalent universe U, we…

$\infty$-topos 中单纯对象的定向单值性

Directed univalence for simplicial objects in an $\infty$-topos

本文在 $\infty$-topos 中单纯对象的语义框架下验证了定向单值性公理，构造了泛左纤维化中同伦类型与函数类型之间的等价。