相关论文: Topological and simplicial models of identity type…

We give a new construction of the model structure on the category of simplicial sets for homotopy $n$-types, originally due to Elvira-Donazar and Hernandez-Paricio, using a right transfer along the coskeleton functor. We observe that an…

In this paper, we introduce a simplicial analog of classifying spaces for commutativity which classify principal bundles with commutativity structure on their transition functions. Our construction $\overline W(\tau,K)$, which takes as…

A new approach to the semantics of identity types in intensional Martin-L\"of type theory is proposed, assuming only a category with finite limits and an interval. The specification of \emph{extensional} identity types in the original…

We define the notion of {\em classifying space} of a topological stack and show that every topological stack \X has a classifying space X which is a topological space well-defined up to weak homotopy equivalence. Under a certain…

This is the second in a series of papers extending Martin-L\"{o}f's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I,…

Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the…

2-Theories are a canonical way of describing categories with extra structure. 2-theory-morphisms are used when discussing how one structure can be replaced with another structure. This is central to categorical coherence theory. We place a…

We give a homotopy theoretic characterization of stacks on a site $\cC$ as the {\it homotopy sheaves} of groupoids on $\cC$. We use this characterization to construct a model category in which stacks are the fibrant objects. We compare…

For groups of a topological origin, such as braid groups and mapping class groups, an important source of interesting and highly non-trivial representations is given by their actions on the twisted homology of associated spaces; these are…

This is an exposition of homotopical results on the geometric realization of semi-simplicial spaces. We then use these to derive basic foundational results about classifying spaces of topological categories, possibly without units. The…

The notion of a simplicial set originated in algebraic topology, and has also been utilized extensively in category theory, but until relatively recently was not used outside of those fields. However, with the increasing prominence of…

We provide an axiomatic treatment of Quillen's construction of the model structure on topological spaces to make it applicable to a wider range of settings, including $\Delta$-generated spaces and pseudotopological spaces. We use this…

We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its $\infty$-localisation an elementary $\infty$-topos, that is, a finitely…

For a pointed topological space $X$, we use an inductive construction of a simplicial resolution of $X$ by wedges of spheres to construct a "higher homotopy structure" for $X$ (in terms of chain complexes of spaces). This structure is then…

We introduce some classes of genuine higher categories in homotopy type theory, defined as well-behaved subcategories of the category of types. We give several examples, and some techniques for showing other things are not examples. While…

We define a model structure on the category GCat of small categories with an action by a finite group G by lifting the Thomason model structure on Cat. We show there is a Quillen equivalence between GCat with this model structure and GTop…

The aim of this thesis is to give a concise introduction to homotopy type theory, to Aczel's constructive set theory and to simplicial sets and their homotopy theory in particular referring to their standard model structure, showing some of…

This paper gives an introduction to the homotopy theory of quasi-categories. Weak equivalences between quasi-categories are characterized as maps which induce equivalences on a naturally defined system of groupoids. These groupoids…

Given a diagram of rings, one may consider the category of modules over them. We are interested in the homotopy theory of categories of this type: given a suitable diagram of model categories M(s) (as s runs through the diagram), we…

The homotopy category of a model structure on a weakly idempotent complete additive category is proved to be equivalent to the additive quotient of the category of cofibrant-fibrant objects with respect to the subcategory of…