scholarly journals Univalence for inverse diagrams and homotopy canonicity

2014 ◽  
Vol 25 (5) ◽  
pp. 1203-1277 ◽  
Author(s):  
MICHAEL SHULMAN
Keyword(s):  
Natural Number ◽  
Type Theory ◽  
Homotopy Theory ◽  
Partial Answer ◽  
Syntactic Category ◽  
Simplicial Sets ◽  
New Models ◽  
Universe Of Sets

We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.

scholarly journals Semantics of higher inductive types

2019 ◽  
Vol 169 (1) ◽  
pp. 159-208 ◽  
Author(s):  
PETER LEFANU LUMSDAINE ◽  
MICHAEL SHULMAN
Keyword(s):  
Type Theory ◽  
Homotopy Theory ◽  
Model Category ◽  
Suitable Model ◽  
Simplicial Sets ◽  
James Construction ◽  
Quillen Model Category ◽  
Wide Range ◽  
Inductive Types ◽  
Cartesian Closed

AbstractHigher inductive typesare a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the “synthetic” development of homotopy theory within type theory, as well as in formalising ordinary set-level mathematics in type theory. In this paper, we construct models of a wide range of higher inductive types in a fairly wide range of settings.We introduce the notion ofcell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category hasweakly stable typal initial algebrasfor any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specialises to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction and general localisations.Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed (∞, 1)-category is presented by some model category to which our results apply.

Algebraic Homotopy Theory

1981 ◽  
Vol 33 (2) ◽  
pp. 302-319 ◽  
Author(s):  
J. F. Jardine
Keyword(s):  
Homotopy Type ◽  
Homotopy Theory ◽  
Unique Factorization ◽  
Contravariant Functor ◽  
Unique Factorization Domain ◽  
Simplicial Sets ◽  
Simplicial Set ◽  
Image Position ◽  
Algebraic Homotopy Theory

Kan and Miller have shown in [9] that the homotopy type of a finite simplicial set K can be recovered from its R-algebra of 0-forms A0K, when R is a unique factorization domain. More precisely, if is the category of simplicial sets and is the category of R-algebras there is a contravariant functorwiththe simplicial set homomorphisms from X to the simplicial R-algebra ∇, whereand the faces and degeneracies of ∇ are induced byandrespectively.

scholarly journals A strictly commutative model for the cochain algebra of a space

2020 ◽  
Vol 156 (8) ◽  
pp. 1718-1743
Author(s):  
Birgit Richter ◽  
Steffen Sagave
Keyword(s):  
Homotopy Theory ◽  
Rational Homotopy ◽  
Graded Algebras ◽  
Differential Graded Algebra ◽  
Simplicial Sets ◽  
Differential Graded Algebras ◽  
Chain Complexes ◽  
Simplicial Set ◽  
New Construction ◽  
Integral Version

AbstractThe commutative differential graded algebra $A_{\mathrm {PL}}(X)$ of polynomial forms on a simplicial set $X$ is a crucial tool in rational homotopy theory. In this note, we construct an integral version $A^{\mathcal {I}}(X)$ of $A_{\mathrm {PL}}(X)$. Our approach uses diagrams of chain complexes indexed by the category of finite sets and injections $\mathcal {I}$ to model $E_{\infty }$ differential graded algebras (dga) by strictly commutative objects, called commutative $\mathcal {I}$-dgas. We define a functor $A^{\mathcal {I}}$ from simplicial sets to commutative $\mathcal {I}$-dgas and show that it is a commutative lift of the usual cochain algebra functor. In particular, it gives rise to a new construction of the $E_{\infty }$ dga of cochains. The functor $A^{\mathcal {I}}$ shares many properties of $A_{\mathrm {PL}}$, and can be viewed as a generalization of $A_{\mathrm {PL}}$ that works over arbitrary commutative ground rings. Working over the integers, a theorem by Mandell implies that $A^{\mathcal {I}}(X)$ determines the homotopy type of $X$ when $X$ is a nilpotent space of finite type.

scholarly journals Integral almost square-free modular categories

2017 ◽  
Vol 16 (06) ◽  
pp. 1750104 ◽  
Author(s):  
Jingcheng Dong ◽  
Libin Li ◽  
Li Dai
Keyword(s):  
Natural Number ◽  
Prime Number ◽  
Partial Answer ◽  
Dimension Formula ◽  
Modular Category ◽  
Number Formula

We study integral almost square-free modular categories; i.e., integral modular categories of Frobenius–Perron dimension [Formula: see text], where [Formula: see text] is a prime number, [Formula: see text] is a square-free natural number and [Formula: see text]. We prove that, if [Formula: see text] or [Formula: see text] is prime with [Formula: see text], then they are group-theoretical. This generalizes several results in the literature and gives a partial answer to the question posed by the first author and Tucker. As an application, we prove that an integral modular category whose Frobenius–Perron dimension is odd and less than [Formula: see text] is group-theoretical.

scholarly journals W-types in homotopy type theory

2014 ◽  
Vol 25 (5) ◽  
pp. 1100-1115 ◽  
Author(s):  
BENNO VAN DEN BERG ◽  
IEKE MOERDIJK
Keyword(s):  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Detailed Account ◽  
Simplicial Sets ◽  
Homotopy Type Theory ◽  
Simplicial Presheaves ◽  
Models Of Set Theory

We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of simplicial presheaves and an application to models of set theory.

scholarly journals Dwyer–Kan homotopy theory for cyclic operads

2021 ◽  
pp. 1-30
Author(s):  
Gabriel C. Drummond-Cole ◽  
Philip Hackney
Keyword(s):  
Homotopy Theory ◽  
Forgetful Functor ◽  
General Definition ◽  
Model Structure ◽  
Simplicial Sets ◽  
Explicit Formulae

Abstract We introduce a general definition for coloured cyclic operads over a symmetric monoidal ground category, which has several appealing features. The forgetful functor from coloured cyclic operads to coloured operads has both adjoints, each of which is relatively simple. Explicit formulae for these adjoints allow us to lift the Cisinski–Moerdijk model structure on the category of coloured operads enriched in simplicial sets to the category of coloured cyclic operads enriched in simplicial sets.

scholarly journals Sets in homotopy type theory

2015 ◽  
Vol 25 (5) ◽  
pp. 1172-1202 ◽  
Author(s):  
EGBERT RIJKE ◽  
BAS SPITTERS
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Connected Components ◽  
Homotopy Type Theory ◽  
Universe Of Sets ◽  
Univalent Foundations ◽  
Subobject Classifier ◽  
Theoretical Foundations ◽  
Special Case

Homotopy type theory may be seen as an internal language for the ∞-category of weak ∞-groupoids. Moreover, weak ∞-groupoids model the univalence axiom. Voevodsky proposes this (language for) weak ∞-groupoids as a new foundation for Mathematics called the univalent foundations. It includes the sets as weak ∞-groupoids with contractible connected components, and thereby it includes (much of) the traditional set theoretical foundations as a special case. We thus wonder whether those ‘discrete’ groupoids do in fact form a (predicative) topos. More generally, homotopy type theory is conjectured to be the internal language of ‘elementary’ of ∞-toposes. We prove that sets in homotopy type theory form a ΠW-pretopos. This is similar to the fact that the 0-truncation of an ∞-topos is a topos. We show that both a subobject classifier and a 0-object classifier are available for the type theoretical universe of sets. However, both of these are large and moreover the 0-object classifier for sets is a function between 1-types (i.e. groupoids) rather than between sets. Assuming an impredicative propositional resizing rule we may render the subobject classifier small and then we actually obtain a topos of sets.

scholarly journals Homotopy theory of complete Lie algebras and Lie models of simplicial sets

2018 ◽  
Vol 11 (3) ◽  
pp. 799-825
Author(s):  
Urtzi Buijs ◽  
Yves Félix ◽  
Aniceto Murillo ◽  
Daniel Tanré
Keyword(s):  
Lie Algebras ◽  
Homotopy Theory ◽  
Simplicial Sets

scholarly journals Model structure on the universe of all types in interval type theory

2020 ◽  
pp. 1-32
Author(s):  
Simon Boulier ◽  
Nicolas Tabareau
Keyword(s):  
Type Theory ◽  
Homotopy Theory ◽  
Model Structure ◽  
Model Categories ◽  
Model Interpretation ◽  
Slight Generalization ◽  
Cubical Sets ◽  
Definition Of ◽  
Interval Type ◽  
The Universe

Abstract Model categories constitute the major context for doing homotopy theory. More recently, homotopy type theory (HoTT) has been introduced as a context for doing syntactic homotopy theory. In this paper, we show that a slight generalization of HoTT, called interval type theory (⫿TT), allows to define a model structure on the universe of all types, which, through the model interpretation, corresponds to defining a model structure on the category of cubical sets. This work generalizes previous works of Gambino, Garner, and Lumsdaine from the universe of fibrant types to the universe of all types. Our definition of ⫿TT comes from the work of Orton and Pitts to define a syntactic approximation of the internal language of the category of cubical sets. In this paper, we extend the work of Orton and Pitts by introducing the notion of degenerate fibrancy, which allows to define a fibrant replacement, at the heart of the model structure on the universe of all types. All our definitions and propositions have been formalized using the Coq proof assistant.

Sign in / Sign up

Export Citation Format

Share Document