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 -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 -categories. The technical vehicle for this are anodyne maps.
Provide a foundations for a theory of -categories, for any . 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
-topoi
HTT, A.3 simplicial categories
HTT, 1. an overview of higher category theory
HTT, fibrations of simplicial sets
HTT, 5. presentable and accessible infinity-categories
HTT, 6. infinity-topoi?
A Segal condition is a (condition defining a) relation on a functor. In motivating cases these relations describe how a value of the functor may be constructed (up to equivalence) by values of subobjects- or truncated versions of .
A groupoid object in is a simplicial object in an (∞,1)-category
that satisfies the groupoidal Segal conditions, meaning that for all and all partitions that share a single element , the (∞,1)-functor exhibits an (∞,1)-pullback
Write for the (∞,1)-category of groupoid objects in , the full sub-(∞,1)-category of simplicial objects on the groupoid objects.
An internal precategory in an -topos is a simplicial object in an (∞,1)-category
such that it satifies the Segal condition, hence such that for all exhibits as the (∞,1)-limit / iterated (∞,1)-pullback
Write for the -category of internal pre-categories in , the full sub-(∞,1)-category of the simplicial objects on the internal precategories.
An internal category in an -topos is an internal pre-category such that its core is in the image of the inclusion .
This is called a complete Segal space object in (Lurie, def. 1.2.10).
A directed graph is a presheaf
(…)
(description of this
diagram from
(…)
Complete Segal spaces were originally defined in
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
Jacob Lurie, On the Classification of Topological Field Theories
ncafé, univalence is a Segal condition
This entry draws from
The globe category is defined to be the category with one object in each degree and the globular operators are defined by the identities
A presheaf on is called a globular set or omega graph or -graph.
-graphs with natural transformations as morphisms form a category denoted by .
Let be -category with underlying reflexive -graph for with globular operators given by source, target, and identity.
Then comes with three composition laws
for . Spelled out this means:
: composition of -morphism along -morphisms (i.e.objects)
: composition of -morphisms along -morphisms (i.e.objects), also called horizontal composition.
: composition of -morphisms along -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 -morphism with a -morphism called whiskering.
An -category is defined to be a reflexive graph such that for every triple , the family has the structure of a -category.
Contents:
Batanin’s -operads are described by their operator categories which are called globular theories.
A finite planar level tree ( or for short just a tree) is a graded set endowed with a map decreasing the degree by one and such that all fibers are linearly ordered.
The collection of trees with maps of graded sets commuting with defines a category , called the category of trees.
The finite ordinal we can regard as the 1-level tree with input edges. Hence the simplex category embeds in the tree category .
The following -construction is due to Batanin.
Let be a tree.
A -sector of height is defined to be a cospan
denoted by where and are consecutive vertices in the linear order .
The set of -sector is graded by the height of sectors.
The source of a sector is defined to be where are consecutive vertices.
The target of a sector is defined to be where are consecutive vertices.
To have a source and a target for every sector of we adjoin in every but the highest degree a lest- and a greatest vertex serving as new minimum and maximum for the linear orders . We denote this new tree by and the set of its sectors by and obtain source- and target operators . This operators satisfy
as one sees in the following diagram depicting an “augmented” tree of height
which means that is an -graph (also called globular set).
Now let denote the globe category whose unique object in degree is , and let denotes the linear -level tree.
Then we have is the standard -globe. (Note that the previous diagram corresponds to the standard globe.)
Let be a monomorphism.
is called to be cartesian if
is a pullback for all .
Let be level trees.
(1) Any map is injective.
(2) The inclusions correspond bijectively to cartesian subobjects of .
(3) The inclusions correspond bijectively to plain subtrees of with a specific choice of -sector for each input vertex of . (…)
(1) The category defined by having as objects the level trees and as morphisms the maps between the associated -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 such that
is an inclusion of a wide subcategory such that representable presheaves on restrict to sheaves on .
(3) Presheaves on which restrict to sheaves on are called -models.
The forgetful functor
is an equivalence of categories.
Let and show that iff by writing as a colimit of representables.
There is a monad on defined by
is induced by Yoneda:
It is not necessary for a functor to have an adjoint to canonically associate a monad to it. The codensity monad of a functor (if it exists) is the right Kan extension of along itself.
啊
A type category is defined to be a category satisfying the following conditions:
(1) For each object there is a collection whose elements are called -indexed types in .
(2) For each object operations assigning to each -indexed type an object called the total object of , together with a morphism
called the projection morphism of .
(3) For each morphism in , an operation assigning to each -indexed type , a indexed type called the pullback of along , together with a morphism making the following a pullback square in the category .
In addition the following strictness conditions will be imposed
This entry is about
The bibliography lists many articles of Robert Goldblatt and Bart Jacobs on modal logic.
(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)
(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 -valued functor inductively defined by
where denotes the identity functor, denotes the constant functor on an object , denotes the coproduct functor of two polynomial functors, and likewise for the product functor, denotes the exponent functor .
A Kripke polynomial functor is inductively defined by
where denotes the composition of a polynomial functor with the power set functor .
(…)
(p.392) Kripke frames are -coalgebras, and Kripke models are coalgebras for the functor .
Explanation: see modal logic
(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.
Let be a set of formulas.
where and likewise . Then we have
Let be a modal model in coalgebraic shape(§9 Example 143). Then iff belongs to the relation lifting (§11) of the satisfaction relation : Every must hold at some successor , and at every successor of some must hold.
The previous lines are the founding insights to coalgebraic logic in which the same principle is applied to an arbitrary set functor and the basic idea is to have
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
For the existence of the language of coalgebraic formulas for it is necessary to allow class based algebras. This may be accomplished by letting be the unique extension of to a set based functor on the category 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.
The initial algebra of the functor is called the language of coalgebraic formulas for and is denoted by
Unwinding this definition yields the following equivalent characterization.
Let 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 is defined to be the least class such that
(1) implies .
(2) implies .Let is the unique extension of to a set based functor on the category having classes as objects and set-continuous (standard) set functors as morphisms.
Let be a functor, let be some natural transformation, let be some collection of natural transformations . then is the standard modal language obtained by taking as the collection off propositional variables, and as the modal similarity type.
Predicate liftings (from can be used to obtain modal operators.
A predicate lifting for a set functor is a natural transformation where denotes the contravariant power set functor. Which each predicate lifting we can associate a modal operator with the following semantics:
For polynomial functors see also the references at polynomial functor. In particular
(Joachim) Kock, Joyal, Batanin, Mascari, Polynomial functors and opetopes, arXiv:0706.1033
Joachim Kock. Polynomial functors and trees. Preprint, arXiv:0807.2874
Nicola Gambino and Joachim Kock (2009); Polynomial functors and polynomial monads; arXiv.
Let us be in a -category . Part of the structure of an idempotent monad in is of course an idempotent morphism . More precisely (Definition 1.1.9) considers as part of the structure such that an idempotent 1-cell has a 2-isomorphism such that . Equivalently an idempotent morphism is a normalized pseudofunctor from the two object monoid with to .
Recall that a splitting of an idempotent consists of a pair of 1-cells and and a pair of 2-isomorphisms and such that where denotes horizontal composition of 2-cells. Equivalently a splitting of an idempotent is a limit or a colimit of the defining pseudofunctor. If has equalizers or coequalizers, then all its idempotents split.
Now if is a splitting of an idempotemt monad, then are adjoint. And in this case the splitting of an idempotent is equivalently an Eilenberg-Moore object for the monad . In this case is called an adjoint retract of .
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.
Proposition 4.5.8, p.209: characterizes “every mono in factors (not necessarily uniquely) as a -closed followed by a -dense.”
Let be a diagram in a category ; a diagram of this type is called a container or a indexed container. Let , , denote base change resp. dependent product resp. dependent sum. Then the composite
which we denote by , is called a polynomial functor. If is the identity we call a linear polynomial functor. This construction exists e.g. if is locally cartesian closed.
If we consider as a semantics for a type theory we can ask how 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 , this preserves display maps if is a display maps and these are closed under composition. forms pullbacks along , and forms exponential objects. In particular for to preserve display maps it is sufficient that and are display maps.
A polynomial functor where (but not necessarily ) 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 is a display map, then
(2a) If (the corresponding polynomial functor is then constant) and is a display map, then the initial algebra of the polynomial functor is . In particular the functor for identity types is of this form.
(2b) If in (2a) is not a display map, then the initial algebra of is a map equipped with a map over with the property that every other map over with a display map, factors through .
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 . In particular the identity type of is the homotopy fiber of the diagonal .
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.
A basic example is the free-monoid monad, Example 1.9. It is exhibited by the polynomial where the middle arrow is such that for all its fiber over has cardinality .
One can construct the free monad on a polynomial endofunctor.
An extensive category (which in particular has finite sums) has W-types iff every polynomial functor in a single variable on 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.
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 -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 -types and some more general cases) remedied by replacing “initial” by “homotopy initial”. This is the main result (to be found in §2) of
The four standard forms of typing judgements are
(1)
(2) definitional equality for types
(3)
(4) definitional equality for termes
There is also another notion of equality - namely propositional equality:
(1) -formation rule
(2) -introduction rule
(3) -elimination rule
(4) -computation rule
One important effect of not having the identity-reflection rule
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 dependent type theory is defined to have -in addition to the standard structural rules- the folowing rules:
(1) the rules for identity types.
(2) rules for -types as presented in Nordstrom-Petterson-Smith §5.8
(3) rules for -types as presented in Garner §3.2
(4) the propositional -rule for -types: the rule asserting that for every $f:(\Pi x:A)B(x), the type
is inhabited.
(5) the Function extensionality axiom (FE): the rule asserting that for every , the type
Comments:
In Voevodsky’s Coq files is shown that the -rule for dependent functions and the function extensionality principle imply the corresponding function extensionality principle for -types. is inhabited.
The function extensionality axiom (FE) is implied by the univalence axiom. The system does not have a global extensionality rule such as the identity reflection rule K or UIP
The transport function: An identity term is interpreted as a path between the points and . More generally an identity term with free variable 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
and an identity term , there is a transport function
For the function is obtained by -elimination.
(…)
The rules for -types in extensional type theory are from the notes to Martin-Löf’s lecture on intuitionistic type theories.
(1) -formation rule
In the following we will sometimes abbreviate by
(2) -introduction rule
(3) -elimination rule
(4) -computation rule
Comments:
We can think of -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 as operations and in which the arity of is the cardinality of the type .
(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 denote the type theory obtained form by adopting the identity reflection rule and let denote the category types as objects and function types 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]] defined by
A -algebra is a pair where is a type and is a function called the structure map of the algebra.
The formation rule gives us an object .
The introduction rule combined with the rule for -types and -types determines a structure map .
The elimination rule implies that the projection where has a section if the type has a -algebra structure over
The computation rule states that the section determined by the elimination rule is also a -algebra homomorphism.
The previous elimination rule implies the simple $W-elimination rule
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.