Spahn 2022-11-30T05:31:01Z tag:ncatlab.org,2012-05-29:Spahn An Instiki Wiki Instiki a reading guide to HTT 2022-11-30T05:31:01Z 2012-06-20T12:52:08Z tag:ncatlab.org,2012-06-20:Spahn,a+reading+guide+to+HTT Anonymous

Contents

This entry is about the text

This book has prerequisites: category theory (see also the exposition in appendix A.1), in particular realization and nerve.

The reading strategy outlined here is approximately the following:

  • Start with appendix A.2.

  • Continue with the overview chapter 1.

  • Chapter 2 developes the theory of fibrations of simplicial sets.The aims of this are mainly three different concerns:

    • Establishing the \infty-Grothendieck construction: The type of fibrations accomplishing this are left/right fibrations (aka. fibrations in groupoids) and cartesian fibrations (aka. Grothendieck fibrations).

    • Preparing the Joyal model structure: This is a foundational topic; the fibrant objects of this model structure are precisely \infty-categories. The technical vehicle for this are anodyne maps.

    • Provide a foundations for a theory of nn-categories, for any nn\le\infty. For the well definedness of this notion minimal fibrations (a special kind of inner fibrations) are introduced.

  • Omit chapter 3.

  • The rest of the book is concerned with constructions which in most cases are proposed in chapter 2. So concentrate on the following important topics:

    • the Grothendieck construction (already in chapter 2), Grothendieck construction in HTT

    • the Yoneda lemma and presheaves, Yoneda lemma in HTT?

    • limits and colimits

    • ind-objects

    • adjoint functors

    • \infty-topoi

A.2 Model categories

HTT, A.2 model categories

A.3 Simplicial categories

HTT, A.3 simplicial categories

1. An overview of higher category theory

HTT, 1. an overview of higher category theory

2. Fibrations of simplicial sets

HTT, fibrations of simplicial sets

4. Limits and colimits

HTT, 4. limits and colimits

5. Presentable and accessible \infty-categories

HTT, 5. presentable and accessible infinity-categories

6. \infty-Topoi

HTT, 6. infinity-topoi?

Segal condition 2022-06-11T10:54:33Z 2012-11-01T17:40:47Z tag:ncatlab.org,2012-11-01:Spahn,Segal+condition Christian Sattler

Idea

A Segal condition is a (condition defining a) relation on a functor. In motivating cases these relations describe how a value F(A)F(A) of the functor FF may be constructed (up to equivalence) by values of subobjects- or truncated versions of AA.

Examples

Example

A groupoid object in 𝒞\mathcal{C} is a simplicial object in an (∞,1)-category

X:Δ op𝒞 X : \Delta^{op} \to \mathcal{C}

that satisfies the groupoidal Segal conditions, meaning that for all nn \in \mathbb{N} and all partitions [n]SS[n] \simeq S \cup S' that share a single element SS={s}S \cap S' = \{s\}, the (∞,1)-functor XX exhibits an (∞,1)-pullback

X([n])X(S)× X(SS)X(S). X([n]) \simeq X(S) \times_{X(S \cap S')} X(S') \,.

Write Grpd(𝒞)Grpd(\mathcal{C}) for the (∞,1)-category of groupoid objects in 𝒞\mathcal{C}, the full sub-(∞,1)-category of simplicial objects on the groupoid objects.

Example

An internal precategory XX in an (,1)(\infty,1)-topos 𝒞\mathcal{C} is a simplicial object in an (∞,1)-category

X:Δ op𝒞 X : \Delta^{op} \to \mathcal{C}

such that it satifies the Segal condition, hence such that for all nn \in \mathbb{N} XX exhibits X([n])X([n]) as the (∞,1)-limit / iterated (∞,1)-pullback

X([n])X({0,1})× X([0])× X[0]X({n1,n}). X([n]) \simeq X(\{0,1\}) \times_{X([0])} \cdots \times_{X[0]} X(\{n-1,n\}) \,.

Write PreCat(𝒞)Pre Cat(\mathcal{C}) for the (,1)(\infty,1)-category of internal pre-categories in 𝒞\mathcal{C}, the full sub-(∞,1)-category of the simplicial objects on the internal precategories.

Definition

An internal category in an (,1)(\infty,1)-topos 𝒞\mathcal{C} is an internal pre-category XXsuch that its core Core(X)Core(X) is in the image of the inclusion 𝒞Grpd(𝒞)\mathcal{C} \hookrightarrow Grpd(\mathcal{C}).

This is called a complete Segal space object in (Lurie, def. 1.2.10).

General theory

A directed graph is a presheaf

D:{1d 1d 00} opSetD:\{1 \stackrel{\overset{d_0}{\leftarrow}}{\underset{d_1}{\leftarrow}} 0\}^{op}\to Set

(…)

(description of this

Cat Nτ PSh(Δ)sSet U F j * j ! GraphSh(Δ 0) i *i * PSh(Δ 0) \array{ Cat &\stackrel{\overset{\tau}{\leftarrow}}{\underoverset{N}{\bottom}{\hookrightarrow}}& PSh(\Delta) \simeq sSet \\ {}^{\mathllap{U}}\downarrow \vdash \uparrow^{\mathrlap{F}} && {}^{\mathllap{j^*}}\downarrow \vdash \uparrow^{\mathrlap{j_!}} \\ Graph \simeq Sh(\Delta_0) &\stackrel{\overset{i^*}{\leftarrow}}{\underoverset{i_*}{\bottom}{\hookrightarrow}}& PSh(\Delta_0) }

diagram from

(…)

References

Complete Segal spaces were originally defined in

  • Charles Rezk, A model for the homotopy theory of homotopy theory , Trans. Amer. Math. Soc., 353(3), 973-1007 (pdf)

The relation to quasi-categories is discussed in

A survey of the definition and its relation to equivalent definitions is in section 4 of

See also pages 29 to 31 of

Clemens Berger, A Cellular Nerve for Higher Categories 2022-06-11T10:44:13Z 2012-11-17T01:58:15Z tag:ncatlab.org,2012-11-17:Spahn,Clemens+Berger%2C+A+Cellular+Nerve+for+Higher+Categories Christian Sattler

This entry draws from

  • Clemens Berger, A cellular nerve for higher categories, Advances in Mathematics 169, 118-175 (2002) (pdf)

0. Notation and terminology

0.1

0.2 Higher graphs and higher categories

Definition

The globe category GG is defined to be the category with one object in each degree and the globular operators s,ts,t are defined by the identities

ss=st s\circ s=s\circ t
tt=tst\circ t= t\circ s

A presheaf on GG is called a globular set or omega graph or ω\omega-graph.

ω\omega-graphs with natural transformations as morphisms form a category denoted by omegaGraph\omegaGraph.

Definition (Godement´s interchange rules)

Let CC be 22-category with underlying reflexive 22-graph C iC_i for i=0,1,2i=0,1,2 with globular operators given by source, target, and identity.

Then (C i) i(C_i)_i comes with three composition laws

i j:C j× iC jC j \circ_i^j: C_j\times_i C_j\to C_j

for 0i<j20\le i\lt j\le 2. Spelled out this means:

i=0,j=1i=0, j=1: composition of 11-morphism along 00-morphisms (i.e.objects)

i=0,j=2i=0,j=2: composition of 22-morphisms along 00-morphisms (i.e.objects), also called horizontal composition.

i=1,j=2i=1,j=2: composition of 22-morphisms along 11-morphisms, also called vertical composition.

Then Godement´s interchange rule or Godement´s interchange law or just interchange law is the assertion that the immediate diagrams commute.

Note that there is on more type of composition of a 11-morphism with a 22-morphism called whiskering.

Definition (ω\omega-category)

An ω\omega-category is defined to be a reflexive graph (C i) i(C_i)_i such that for every triple i<j<ki\lt j\lt k, the family (C i,C j,C k; i j, i k, j )(C_i,C_j,C_k;\circ_i^j,\circ_i^k, \circ_j^) has the structure of a 22-category.

1. Globular theories and cellular nerves

Contents:

Batanin’s ω\omega-operads are described by their operator categories which are called globular theories.

Definition (finite planar level tree)

A finite planar level tree ( or for short just a tree) is a graded set (T(n)) n 0(T(n))_{n\in \mathbb{N}_0} endowed with a map i T:T >0i_T: T_{\gt 0} decreasing the degree by one and such that all fibers i T 1(x)i_T^{-1}(x) are linearly ordered.

The collection of trees with maps of graded sets commuting with ii defines a category 𝒯\mathcal{T}, called the category of trees.

Example

The finite ordinal [n]Δ[n]\in \Delta we can regard as the 1-level tree with nn input edges. Hence the simplex category embeds in the tree category Δ𝒯\Delta\hookrightarrow\mathcal{T}.

The following *{}_*-construction is due to Batanin.

Lemma and Definition (ω\omega-graph of sectors of a tree)

Let TT be a tree.

A TT-sector of height kk is defined to be a cospan

y y y\array{ y^\prime&&y^{\prime\prime} \\ \searrow&&\swarrow \\ &y }

denoted by (y;y ,y )(y;y^\prime,y^{\prime\prime}) where yT(k)y\in T(k) and y<y y\lt y^{\prime\prime} are consecutive vertices in the linear order i T 1(y)i_T^{-1}(y).

The set GTGT of TT-sector is graded by the height of sectors.

The source of a sector (y;y ,y )(y;y^\prime,y^{\prime\prime}) is defined to be (i(y);x,y)(i(y);x,y) where x,yx,y are consecutive vertices.

The target of a sector (y;y ,y )(y;y^\prime,y^{\prime\prime}) is defined to be (i(y);y,z)(i(y);y,z) where y,zy,z are consecutive vertices.

y y x y z i i(y)\array{ &y^\prime&&y^{\prime\prime} \\ & \searrow&&\swarrow \\ x&&y&&z \\ \searrow&&\downarrow^i&&\swarrow \\ &&i(y) }

To have a source and a target for every sector of TT we adjoin in every but the highest degree a lest- and a greatest vertex serving as new minimum and maximum for the linear orders i 1(x)i^{-1}(x). We denote this new tree by T¯\overline T and the set of its sectors by T *:=GT¯(k)T_*:=G\overline T(k) and obtain source- and target operators s,t:T *T *s,t:T_*\to T_*. This operators satisfy

ss=sts\circ s=s\circ t
tt=tst\circ t =t\circ s

as one sees in the following diagram depicting an “augmented” tree of height 33

T(3) y y T(2) x y z i T(1) u v w i T(0) r\array{ T(3)&&&y^\prime&&y^{\prime\prime} \\ &&& \searrow&&\swarrow \\ T(2)&&x&&y&&z \\ &&\searrow&&\downarrow^i&&\swarrow \\ T(1)&&u&&v&&w \\ &&\searrow&&\downarrow^i&&\swarrow \\ T(0)&&&&r }

which means that T *T_* is an ω\omega-graph (also called globular set).

Now let GG denote the globe category whose unique object in degree nn\in \mathbb{N} is n Gn_G, and let n\mathbf{n} denotes the linear nn-level tree.

Then we have n *G(,n G)\mathbf{n}_*\simeq G(-,n_G) is the standard nn-globe. (Note that the previous diagram corresponds to the standard 33 globe.)

Definition

Let f:S *T *f:S_*\to T_* be a monomorphism.

ff is called to be cartesian if

(S *) n f n (T *) n s t (S *) n1 f n1 (T *) n1\array{ (S_*)_n&\stackrel{f_n}{\to}&(T_*)_n \\ \downarrow^s&&\downarrow^t \\ (S_*)_{n-1}&\stackrel{f_{n-1}}{\to}&(T_*)_{n-1} }

is a pullback for all nn.

Lemma

Let S,TS,T be level trees.

(1) Any map S *T *S_*\to T_* is injective.

(2) The inclusions S *T *S_*\hookrightarrow T_* correspond bijectively to cartesian subobjects of T *T_*.

(3) The inclusions S *T *S_*\hookrightarrow T_* correspond bijectively to plain subtrees of TT with a specific choice of TT-sector for each input vertex of SS. (…)

Definition

(1) The category Θ 0\Theta_0 defined by having as objects the level trees and as morphisms the maps between the associated ω\omega-graphs. These morphisms are called immersions. This category shall be equipped with the structure of a site by defining the covering sieves by epimorphic families (of immersions). This site is called the globular site.

(2) A globular theory is defined to be a category Θ A\Theta_A such that

Θ 0Θ A\Theta_0\hookrightarrow \Theta_A

is an inclusion of a wide subcategory such that representable presheaves on Θ A\Theta_A restrict to sheaves on Θ 0\Theta_0.

(3) Presheaves on Θ A\Theta_A which restrict to sheaves on Θ 0\Theta_0 are called Θ A\Theta_A-models.

Lemma

The forgetful functor

Sh(Θ 0)ωGraph:=Psh(G)Sh (\Theta_0)\to \omega Graph:=Psh (G)

is an equivalence of categories.

Proof

Let XPsh(Θ 0)X\in Psh(\Theta_0) and show that XSh(Θ 0)X\in Sh(\Theta_0) iff X(T)hom Psh(G)(T *,X)X(T)\simeq hom_{Psh(G)}(T_*,X) by writing XX as a colimit of representables.

Definition

There is a monad (w,η,μ)(w,\eta,\mu) on ωGraph\omega Graph defined by

w(X) n:= T:ht(T)nhom ωGraph(T *,X)w(X)_n:=\coprod_{T:ht(T)\le n}hom_{\omega Graph}(T_*,X)

η:id Psh(G)w\eta:id_{Psh(G)}\to w is induced by Yoneda: X nhom ωGraph(n *,X)X_n\mapsto hom_{\omega Graph}(n_*,X)

2. Cellular sets and their geometric realization

3. A closed model structure for cellular sets

4. Homotopy structure for weak ω\omega-categories

codensity monad 2018-10-19T12:32:33Z 2012-12-27T04:50:56Z tag:ncatlab.org,2012-12-27:Spahn,codensity+monad Todd Trimble

It is not necessary for a functor to have an adjoint to canonically associate a monad to it. The codensity monad of a functor FF (if it exists) is the right Kan extension of FF along itself.

References

  • Tom Leinster,
    • where do monads come from?, post to the n-Café, web
    • codensity and the ultrafilter monad, arXiv:1209.3606
universal polynomial 2017-02-23T06:51:06Z 2017-02-23T06:51:06Z tag:ncatlab.org,2017-02-23:Spahn,universal+polynomial Anonymous

universal polynomial

My First Slide

kirelagin 2014-12-12T12:15:26Z 2014-12-12T12:06:37Z tag:ncatlab.org,2014-12-12:Spahn,kirelagin kirelagin
type category 2014-12-12T12:05:58Z 2012-12-25T06:14:15Z tag:ncatlab.org,2012-12-25:Spahn,type+category kirelagin
Definition

A type category is defined to be a category satisfying the following conditions:

(1) For each object XCX\in C there is a collection Type C(X)Type_C(X) whose elements are called XX-indexed types in CC.

(2) For each object XCX\in C operations assigning to each XX-indexed type AA an object XAX \ltimes A called the total object of AA, together with a morphism

p A:XAXp_A:X \ltimes A \to X

called the projection morphism of AA.

(3) For each morphism f:YXf:Y\to X in CC, an operation assigning to each XX-indexed type AA, a YY indexed type f *Af^* A called the pullback of AA along XX, together with a morphism fA:Yf *AXAf\ltimes A:Y\ltimes f^* A\to X\ltimes A making the following a pullback square in the category CC.

Yf *A fA XA p f *A p A Y fX\array{ Y\ltimes f^* A&\stackrel{f\ltimes A}{\to}&X\ltimes A \\ \downarrow^{p_{f^* A}}&&\downarrow^{p_A} \\ Y&\stackrel{f}{\to} X }

In addition the following strictness conditions will be imposed

id X *A=Aid^*_X A=A
id XA=id XAid_X\ltimes A=id_{X\ltimes A}
g *(f *A)=(fg) *Ag^*(f^* A)=(f\circ g)^* A
(fA)(gf *A)=(fg)A(f\ltimes A)\circ (g\ltimes f^* A)=(f\circ g)\ltimes A

Reference

  • Pitts, Andrew M. Categorical logic. Handbook of logic in computer science, Vol. 5, 39–128, Handb. Log. Comput. Sci., 5, Oxford Univ. Press, New York, 2000. pdf, chapter 6.3
algebraic- and coalgebraic semantics of modal logic 2013-05-19T18:31:29Z 2013-02-16T03:43:23Z tag:ncatlab.org,2013-02-16:Spahn,algebraic-+and+coalgebraic+semantics+of+modal+logic Stephan Alexander Spahn

This entry is about

  • Yde Venema, Algebras and Coalgebras, §6 (p.332-426)in Blackburn, van Benthem, Wolter, Handbook of modal logic, Elsevier, 2007.

The bibliography lists many articles of Robert Goldblatt and Bart Jacobs on modal logic.

1 Introduction

(p.332)

(…)

An important difference of the coalgebraic approach compared to the algebraic one is that coalgebras generalize rather than dualize the model theory of modal logic. One may generalize the concept of modal logic from Kripke frames to arbitrary coalgebras. In fact the link between modal logic and coalgebra is so strong that one may claim that modal logic is the natural logic for coalgebras (just like equational logic is that for algebra)

9 Coalgebras: an introduction

(p.389)

The notion of coalgebra was formed in the sixties but the topic attracted a wider attention only when was realized that coalgebras can be seen as a general uniform theory of dynamic systems.

We list some applications (or examples) of the theory of coalgebras.

  • The main examples for coalgebras are Kripke frames.

  • Aczel in [non-well founded sets] models transition systems and non-well founded sets as coalgebras.

  • Barwise-Moss in [Vicious Circles] discuss notions of circularity and self-reference (and many (other) applications).

  • Rutten [Automata and coinduction] on coalgebras and deterministic automata.

(Definition 146, p.392) A polynomial functor is a SetSet-valued functor inductively defined by

K::=I|C|K 0+K 1|K 0×K 1|K DK::=I | C | K_0 + K_1 | K_0\times K_1 | K^D

where II denotes the identity functor, CC denotes the constant functor on an object CC, K 0+K 1K_0 +K_1 denotes the coproduct functor of two polynomial functors, and likewise for the product functor, K DK^D denotes the exponent functor XK(X) DX\mapsto K(X)^D.

A Kripke polynomial functor is inductively defined by

K::=I|C|K 0+K 1|K 0×K 1|K D|PKK::=I | C | K_0 + K_1 | K_0\times K_1 | K^D | P K

where PKP K denotes the composition of a polynomial functor KK with the power set functor PP.

(…)

(p.392) Kripke frames are PIPI-coalgebras, and Kripke models are coalgebras for the functor PProp×PIPProp\times PI.

Explanation: see modal logic

13 Modal logic and coalgebras

(p.406)

The initial ideas in this section are attributed to L. Moss:

  • Coalgebraic logic. Annals of Pure and Applied Logic, 96:277–317, 1999. (Erratum published Ann.P.Appl.Log. 99:241–259, 1999).

  • J. Barwise and L. Moss. Vicious Circles, volume 60 of CSLI Lecture Notes. CSLI Publications, 1996.

Introduction

Let ϕ\phi be a set of formulas.

ϕ:=ϕϕ\nabla \phi:=\Box\bigvee \phi \wedge \bigwedge \diamond\phi

where ϕ:={φ|φϕ}\diamond \phi:=\{\diamond \varphi|\varphi\in \phi\} and likewise ϕ\Box\phi. Then we have

φ{φ,}\diamond\varphi \simeq \nabla\{\varphi,\top\}
φ{φ}\Box \varphi\simeq\nabla\varnothing\vee\nabla\{\varphi\}

Let 𝕊:=S,λ,R[]\mathbb{S}:=\langle S,\lambda,R[\cdot]\rangle be a modal model in coalgebraic shape(§9 Example 143). Then 𝕊,sϕ\mathbb{S},s\Vdash\nabla \phi iff (R[s],ϕ)(R[s],\phi) belongs to the relation lifting (§11) 𝒫¯( 𝕊)\overline{\mathcal{P}}(\Vdash_{\mathbb{S}}) of the satisfaction relation 𝕊S×ϕ\Vdash_{\mathbb{S}}\subseteq S\times \phi: Every φΦ\varphi\in \Phi must hold at some successor tR[s]t\in R[s], and at every successor tt of some φϕ\varphi\in \phi must hold.

The previous lines are the founding insights to coalgebraic logic in which the same principle is applied to an arbitrary set functor Ω\Omega and the basic idea is to have

𝕊,s 𝕊Piff(P,σ(s))Ω¯( 𝕊).\mathbb{S},s\Vdash_{\mathbb{S}}\nabla P\;\text{iff}\; (P,\sigma(s))\in \overline{\Omega}(\Vdash_{\mathbb{S}}).

In this situation, the satisfaction relation is much like a bisimulation between a language and a coalgebra; for this see

  • A. Baltag. A logic for coalgebraic simulation. In

    • H. Reichel, editor. Coalgebraic Methods in Computer Science (CMCS’00), volume 33 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000.

Definition

For the existence of the language of coalgebraic formulas for Ω\Omega it is necessary to allow class based algebras. This may be accomplished by letting Ω +\Omega^+ be the unique extension of Ω\Omega to a set based functor on the category SETSET having classes as objects and set-continuous (standard) set functors as morphisms. In examples these functors are often polynomial functors; e.g. Kripke functors are of this kind.

Definition

The initial algebra of the functor (P+Ω) +(P+\Omega)^+ is called the language of coalgebraic formulas for Ω\Omega and is denoted by

Ω,,.\langle\mathcal{L}_\Omega, \bigwedge,\nabla\rangle.

Unwinding this definition yields the following equivalent characterization.

Definition

Let Ω:SetSet\Omega:Set\to Set be (for convenience) be a set functor sending inlusions to inclusions (call this a standard set functor). Then the language of coalgebraic formulas denoted by Ω\mathcal{L}_\Omega is defined to be the least class CC such that

(1) ϕ Ω\phi\in \mathcal{L}_\Omega implies ϕ Ω\bigwedge\phi\in \mathcal{L}_\Omega.

(2) PΩ +( Ω)P\in \Omega^+(\mathcal{L}_\Omega) implies P Ω\nabla P\in \mathcal{L}_\Omega.Let Ω +\Omega^+ is the unique extension of Ω\Omega to a set based functor on the category SETSET having classes as objects and set-continuous (standard) set functors as morphisms.

Definition (p.411)

Let Ω:SetSet\Omega:\Set\to Set be a functor, let ν:ΩProp\nu:\Omega\to Prop be some natural transformation, let \bigwedge be some collection of natural transformations Ω𝒫\Omega\to \mathcal{P}. then ν,\mathcal{L}_{\nu,\bigwedge} is the standard modal language obtained by taking PropProp as the collection off propositional variables, and τ :={ λ|λ}\tau_\bigwedge:=\{\diamond_\lambda|\lambda\in \bigwedge\} as the modal similarity type.

Predicate liftings (from 𝒫S𝒫ΩS\mathcal{P} S\to \mathcal{P}\Omega S can be used to obtain modal operators.

Definition (p.412)

A predicate lifting for a set functor Ω\Omega is a natural transformation μ:𝒫ˇ𝒫ˇΩ\mu:\check{\mathcal{P}}\to \check{\mathcal{P}} \Omega where Pˇ\check{P} denotes the contravariant power set functor. Which each predicate lifting we can associate a modal operator μ\diamond_\mu with the following semantics:

𝕊,s λφiffσ(s)μ S([[φ]]).\mathbb{S},s\Vdash \diamond_\lambda \varphi\;\text{iff}\;\sigma(s)\in \mu_S([[\varphi]]).

References

For polynomial functors see also the references at polynomial functor. In particular

idempotent monad 2013-05-02T00:32:05Z 2013-02-18T03:18:10Z tag:ncatlab.org,2013-02-18:Spahn,idempotent+monad Anonymous
Remark

Let us be in a 22-category KK. Part of the structure of an idempotent monad (C,T,η,μ)(C,T,\eta,\mu) in KK is of course an idempotent morphism T:CCT:C\to C. More precisely (Definition 1.1.9) considers μ\mu as part of the structure such that an idempotent 1-cell has a 2-isomorphism μ:TTT\mu:TT\to T such that μT=Tμ\mu T=T\mu. Equivalently an idempotent morphism is a normalized pseudofunctor from the two object monoid {*,e}\{*,e\} with e 2=ee^2=e to KK.

Recall that a splitting of an idempotent (T,μ)(T,\mu) consists of a pair of 1-cells I:DCI:D\to C and R:CDR:C\to D and a pair of 2-isomorphisms a:RIid Da:RI\to id_D and b:TIRb:T\to IR such that μ=b 1(IAR)(bb)\mu=b^{-1}(I\circ A\circ R)(b\circ b) where \circ denotes horizontal composition of 2-cells. Equivalently a splitting of an idempotent is a limit or a colimit of the defining pseudofunctor. If KK has equalizers or coequalizers, then all its idempotents split.

Now if (I,R,a,b)(I,R,a,b) is a splitting of an idempotemt monad, then RIR\dashv I are adjoint. And in this case the splitting of an idempotent is equivalently an Eilenberg-Moore object for the monad (C,T,η,μ)(C,T,\eta,\mu). In this case DD is called an adjoint retract of CC.

Remark

Equivalences (resp. cores) in an allegory are precisely those symmetric idempotents which are idempotent monads (resp. comonads). In an allegory the following statements are equivalent: all symmetric idempotents split, idempotent monads split, idempotent comonads split. A similar statement holds at least for some 2-categories.

References

  • Peter Johnstone, sketches of an elephant, B 1.1.9, p.248-249
aspects of topoi 2013-03-23T04:38:16Z 2013-03-23T04:37:38Z tag:ncatlab.org,2013-03-23:Spahn,aspects+of+topoi Stephan Alexander Spahn

aspects of topoi

notes on elephant 2013-03-02T05:35:59Z 2013-03-02T05:35:46Z tag:ncatlab.org,2013-03-02:Spahn,notes+on+elephant Stephan Alexander Spahn

Proposition 4.5.8, p.209: characterizes “every mono in EE factors (not necessarily uniquely) as a jj-closed followed by a jj-dense.”

polynomial functor 2013-02-28T07:36:58Z 2013-02-28T00:30:38Z tag:ncatlab.org,2013-02-28:Spahn,polynomial+functor Stephan Alexander Spahn

Let WfXgYhZW\stackrel{f}{\leftarrow}X\stackrel{g}{\to}Y\stackrel{h}{\to}Z be a diagram in a category CC; a diagram of this type is called a container or a indexed container. Let f *f^*, Π g\Pi_g, Σ\Sigma denote base change resp. dependent product resp. dependent sum. Then the composite

C/Wf *C/XΠ gC/YΣ hC/ZC/W\stackrel{f^*}{\to}C/X\stackrel{\Pi_g}{\to}C/Y\stackrel{\Sigma_h}{\to}C/Z

which we denote by PP, is called a polynomial functor. If gg is the identity we call PP a linear polynomial functor. This construction exists e.g. if CC is locally cartesian closed.

If we consider CC as a semantics for a type theory we can ask how P=Σ hΠ gf *P=\Sigma_h \Pi_g f^* interacts with display maps: recall that by definition the class of display maps is closed under composition, pullbacks along arbitrary morphisms, and forming exponential objects. Since Σ h=()f\Sigma_h=(-)\circ f, this preserves display maps if hh is a display maps and these are closed under composition. f *f^* forms pullbacks along ff, and Π\Pi forms exponential objects. In particular for PP to preserve display maps it is sufficient that gg and hh are display maps.

A polynomial functor Σ hΠ gf *\Sigma_h\Pi_g f^* where gg (but not necessarily hh) is a display map, restricted to display maps, one could call a dependent polynomial functor or better an inductive polynomial functor.

Initial algebras for polynomial functors, inductive families: A (weakly) initial algebra for an inductive polynomial functor we call an inductive family. An inductive family exists for all inductive polynomial functors.

Examples:

(1) If h=Δ:ZZ×Zh=\Delta:Z\to Z\times Z is a display map, then Id Z(z,z)={refl}Id_Z(z,z)=\{refl\}

(2a) If X=X=\emptyset (the corresponding polynomial functor PP is then constant) and hh is a display map, then the initial algebra of the polynomial functor is hh. In particular the functor for identity types is of this form.

(2b) If in (2a) hh is not a display map, then the initial algebra of PP is a map h^:A^Z\hat h:\hat A\to Z equipped with a map hˇ:hh^\check{h}:h\to \hat h over ZZ with the property that every other map hqh\to q over ZZ with qq a display map, factors through h^\hat h.

The Coq defining an inductive family is

Inductive hfiber {A X} (I: A ->X) : (X->Type):=
inj : forall (x:A), hfiber I(Ix).

It is just the homotopy fiber of II. In particular the identity type of XX is the homotopy fiber of the diagonal Δ:XX×X\Delta:X\to X\times X.

monad on a quasicategory 2013-02-28T04:11:01Z 2013-02-28T03:44:55Z tag:ncatlab.org,2013-02-28:Spahn,monad+on+a+quasicategory Stephan Alexander Spahn
polynomial monad 2013-02-27T23:31:57Z 2013-02-17T05:06:45Z tag:ncatlab.org,2013-02-17:Spahn,polynomial+monad Stephan Alexander Spahn

A polynomial monad is a monad whose underlying endofunctor is a polynomial functor polynomial functor. This is of course equivalent to being a monad in the category of polynomial functors.

Examples

A basic example is the free-monoid monad, Example 1.9. It is exhibited by the polynomial 1 11\leftarrow \mathbb{N}^\prime\rightarrow \mathbb{N}\rightarrow 1 where the middle arrow is such that for all nn\in \mathbb{N} its fiber over nn has cardinality nn.

One can construct the free monad on a polynomial endofunctor.

An extensive category EE (which in particular has finite sums) has W-types iff every polynomial functor in a single variable on EE has an initial algebra. The “W” in the name of this notion refers to the fact Martin-Löf’s types of wellfounded trees (translated into category theory) are initial algebras for polynomial endofunctors in a single variable. Initial algebras for (general) polynomial functors correspond to Petersson-Synek tree types.

Reference

  • Nicola Gambino and Joachim Kock (2009); Polynomial functors and polynomial monads; arXiv.
higher inductive type 2013-02-27T04:15:02Z 2013-02-25T07:32:53Z tag:ncatlab.org,2013-02-25:Spahn,higher+inductive+type Stephan Alexander Spahn

1Categorially a higher inductive type in an extensional type theory is an initial algebra of an endofunctor. In intensional type theory this analogy fails.

In particular WW-types in an extensional type theory correspond to initial algebras of polynomial functors. Also this is not true for intensional type theories.

This failure of intensional type theory can be (at least for WW-types and some more general cases) remedied by replacing “initial” by “homotopy initial”. This is the main result (to be found in §2) of

  • Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, arXiv:1201.3898

Extensional vs. intensional type theories

The four standard forms of typing judgements are

(1) A:TypeA:Type

(2) A=B:TypeA=B:Type definitional equality for types

(3) a:Aa:A

(4) a=b:Aa=b:A definitional equality for termes

There is also another notion of equality - namely propositional equality:

Rules for identity types

(1) IdId-formation rule

A:Typea:Ab:AId A(a,b):Type\frac{A:Type\; a:A\; b:A}{Id_A(a,b):Type}

(2) IdId-introduction rule

a:Arefl(a):Id A(a,a)\frac{a:A}{refl(a):Id_A(a,a)}

(3) IdId-elimination rule

a,y:A,u:Id A(x,y)C(x,y,u):Type x:Ac(x):C(x,x,refl(x))x,y:A,u:Id A(x,y)idrec(x,y,u,c):C(x,y,u)\frac{\array{a,y:A,u:Id_A(x,y)\vdash C(x,y,u):Type\\x:A\vdash c(x):C(x,x,refl(x))}}{x,y:A,u:Id_A(x,y)\vdash idrec(x,y,u,c):C(x,y,u)}

(4) IdId-computation rule

a,y:A,u:Id A(x,y)C(x,y,u):Type x:Ac(x):C(x,x,refl(x))x:Aidrec(x,x,refl(x),c)=c(x):C(x,xrefl(x))\frac{\array{a,y:A,u:Id_A(x,y)\vdash C(x,y,u):Type\\x:A\vdash c(x):C(x,x,refl(x))}}{x:A\vdash idrec(x,x,refl(x),c)=c(x):C(x,xrefl(x))}

One important effect of not having the identity-reflection rule

p:Id A(x,y)x=y:A\frac{p:Id_A(x,y)}{x=y:A}

is that it is impossible to prove that the empty type is an initial object. There are some extensionality principles which are weaker than the identity reflection rule: Streicher’s K-rule, the Uniqueness of Identity Proofs (UIP) which also has benn considered in context of Observational Type Theory. However these constructions seem to be ad hoc and lack a conceptual basis.

The system \mathcal{H}

The dependent type theory \mathcal{H} is defined to have -in addition to the standard structural rules- the folowing rules:

(1) the rules for identity types.

(2) rules for Σ\Sigma-types as presented in Nordstrom-Petterson-Smith §5.8

(3) rules for Π\Pi-types as presented in Garner §3.2

(4) the propositional η\eta-rule for Π\Pi-types: the rule asserting that for every $f:(\Pi x:A)B(x), the type

Id(f,λx,app(f,x),app(g,x))Id AB(f,g)Id(f,\lambda x,app(f,x),app(g,x))\to Id_{A\to B}(f,g)

is inhabited.

(5) the Function extensionality axiom (FE): the rule asserting that for every f,g:ABf,g:A\to B, the type

(Πx:A)Id B(app(f,x),app(g,x)))Id AB(f,g)(\Pi x:A) Id_B(app(f,x),app(g,x)))\to Id_{A\to B}(f,g)

Comments:

In Voevodsky’s Coq files is shown that the η\eta-rule for dependent functions and the function extensionality principle imply the corresponding function extensionality principle for Σ\Sigma-types. is inhabited.

The function extensionality axiom (FE) is implied by the univalence axiom. The system \mathcal{H} does not have a global extensionality rule such as the identity reflection rule K or UIP

Homotopical semantics

The transport function: An identity term p:Id(a,b)p:Id(a,b) is interpreted as a path between the points aa and bb. More generally an identity term p(x):Id(a(x),b(x))p(x):Id(a(x),b(x)) with free variable xx is interpreted as a continuous family of paths, i.e. a homotopy between the continuous functions. The identity elimination rule implies that type dependency respects identity: For a dependent type

x:AB(x):Typex:A\vdash B(x):Type

and an identity term p:Id A(a,b)p:Id_A(a,b), there is a transport function

p !:B(a)B(b).p_!:B(a)\to B(b).

For x:Ax:A the function refl(x) !:B(x)B(x)refl(x)_!:B(x)\to B(x) is obtained by IdId-elimination.

(…)

Extensional WW-types

The rules for WW-types in extensional type theory are from the notes to Martin-Löf’s lecture on intuitionistic type theories.

(1) WW-formation rule

A:Typex:AB(x):Type(Wx:A)B(x):Type\frac{A:Type\; x:A\vdash B(x):Type}{(Wx:A)B(x):Type}

In the following we will sometimes abbreviate (Wx:A)B(x)(Wx:A)B(x) by WW

(2) WW-introduction rule

a:At:B(a)Wsup(a,t):W\frac{a:A\; t:B(a)\to W}{sup(a,t):W}

(3) WW-elimination rule

w:WC(w):Type x:A,u:B(x)W,v:(Πy:B(x))C(u(y)) c(x,y,v):C(sup(x,y))w:Wwrec(w,c):C(w)\frac{\array{w:W\vdash C(w):Type\\ x:A, u:B(x)\to W, v:(\Pi y:B(x))C(u(y))\vdash\\ c(x,y,v):C(sup(x,y))}}{w:W\vdash wrec(w,c):C(w)}

(4) WW-computation rule

w:WC(w):Type x:A,u:B(x)W,v:(Πy:B(x))C(u(y)) c(x,y,v):C(sup(x,y))x:A,u:B(x)Wwrec(sup(x,u),c)= c(x,u,λy.wrec(u(y),c)):C(sup(x,u))\frac{\array{w:W\vdash C(w):Type\\ x:A, u:B(x)\to W, v:(\Pi y:B(x))C(u(y))\vdash\\ c(x,y,v):C(sup(x,y))}}{\array{ x:A, u:B(x)\to W\vdash wrec(sup(x,u),c)=\\ c(x,u,\lambda y.wrec(u(y),c)):C(sup(x,u))}}

Comments:

We can think of WW-types as free algebras for signatures with operations of possibly infinite arity, but no equations:

(ad1) We consider the premises of this rule as specifying a signature which has the elements of AA as operations and in which the arity of a:Aa:A is the cardinality of the type B(a)B(a).

(ad2) Then, the introduction rule -as always- specifies the canonical way of forming an element of the type in consideration.

(ad3) The elimination rule can be interpreted as the propositions-as-types translation of the appropriate induction principle.

In more detail, let ext\mathcal{H}_ext denote the type theory obtained form \mathcal{H} by adopting the identity reflection rule p:Id A(x,y)x=y:A\frac{p:Id_A(x,y)}{x=y:A} and let 𝒞( ext)\mathcal{C}(\mathcal{H}_ext) denote the category types as objects and function types f:ABf:A\to B as morphisms where two maps are considered to be equal if they are definitionally equal.

Then, the premisses of the introduction rule determine the [[nLab:polynomial functor|polynomial endofunctor]] P:𝒞( ext)𝒞( ext)P:\mathcal{C}(\mathcal{H}_ext)\to \mathcal{C}(\mathcal{H}_ext) defined by

P(X)= def(Σx:A)(B(x)X).P(X)=_{def}(\Sigma x: A)(B(x)\to X).

A PP-algebra is a pair (C,s C)(C,s_C) where CC is a type and s C:PCCs_C:PC\to C is a function called the structure map of the algebra.

The formation rule gives us an object W= def(Wx:A)B(x)W=_{def} (Wx:A)B(x).

The introduction rule combined with the rule for Π\Pi-types and Σ\Sigma-types determines a structure map s W:PWWs_W:PW\to W.

The elimination rule implies that the projection π 1:CW\pi_1:C\to W where C= def(Σw:W)C(w)C=_{def} (\Sigma w:W)C(w) has a section ss if the type CC has a PP-algebra structure over WW

The computation rule states that the section ss determined by the elimination rule is also a PP-algebra homomorphism.

PC s C C π 1 s PW s W W \array{ PC&\stackrel{s_C}{\to}&C\\ \downarrow&&\downarrow^{\pi_1}\uparrow_s\\ PW&\stackrel{s_W}{\to}&W& }

The previous elimination rule implies the simple $W-elimination rule

C:Typex:A,v:B(x)Cc(x,v):Cw:Wsimpwrec(w,c):C\frac{C:Type\; x:A,v:B(x)\to C\vdash c(x,v):C}{w:W\vdash simp-wrec(w,c):C}

References

  • Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, arXiv:1201.3898

  • S. Awodey, Type theory and homotopy, pdf

  • T. Streicher, Investigations into intensional type theory, 1993, Habilitation Thesis. Available from the author’s web page.

  • B. Nordstrom, K. Petersson, and J. Smith, Martin-Löf type theory in Handbook of Logic in Computer Science. Oxford Uni- versity Press, 2000, vol. 5, pp. 1–37

  • R. Garner, On the strength of dependent products in the type theory of Martin-Löf, Annals of Pure and Applied Logic, vol. 160, pp. 1–12, 2009.

  • V. Voevodsky, Univalent foundations Coq files, 2010, available from the author’s web page.

  • P. Martin-Löf, Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, 1980. Bibliopolis, 1984.