nLab
HoTT methods for homotopy theorists

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecompositionsubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem

homotopy levels

semantics

This page is meant to be useful for readers who are interested in homotopy theory but not (necessarily) in homotopy type theory as such (its role as a symbolic logic, etc.) but who do care learning about whatever new methods that may make them be better homotopy theorists, and about any new insights into homotopy theory itself that could be gained by applying methods that originate in homotopy type theory. In other words, this page is meant to help answer the question:

I am a homotopy theorist; what can homotopy type theory do for me?

Since homotopy theory takes place in model categories and similar categorical structures, the input from homotopy type theory is via its categorical semantics. In this sense the question which this page is meant to help to answer is

I am a homotopy theorist; which methods can I learn from the categorical semantics of homotopy type theory?

For the moment this page will mostly list pointers with brief comments to other entries where details are given. You should maybe read it like an instructional exercise list and follow the pointers for help.

Contents

Basic dictionary for the internal language

Starting from (homotopy) category theory, the corresponding (homotopy) type theory is simply a formal language for denoting familiar constructions, as indicated in the following table.

(homotopy) category theory(homotopy) type theory
semanticssyntax
object XXtype x:Xx : X
fibration(display map) A p X\array{A \\ \downarrow^{\mathrlap{p}} \\ X}dependent type x:XA(x):Typex : X \vdash A(x) : Type
section X t A id p X\array{ X &&\stackrel{t}{\to}&& A \\ & {}_{\mathllap{id}}\searrow && \swarrow_{p} \\ && X}term x:Xt(x):A(x)x : X \vdash t(x) : A(x)
pullback f *A A p Y f X\array{ f^* A &\to& A \\ \downarrow && \downarrow^{\mathrlap{p}} \\ Y &\stackrel{f}{\to} & X }substitution y:YA(f(y)):Typey : Y \vdash A(f(y)) : Type
direct image A f *A p f *p X f Y\array{ A && f_* A \\ {}^{\mathllap{p}}\downarrow && \downarrow ^{f_* p}\\ X &\stackrel{f}{\to}& Y}dependent product y:Yx:X(y)A(x):Type y : Y \vdash \underset{x : X(y)}{\prod } A(x) : Type
internal hom in slice X×f *A f *f *A =[X,A] Y X f Y\array{ X \times f^* A && f_* f^* A & = [X,A]_Y \\ {}^{\mathllap{}}\downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}function type y:YX(y)A(y):Type y : Y \vdash X(y) \to A(y) : Type
postcomposition A = f !A X f Y\array{ A &=& f_! A \\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}dependent sum y:Yx:X(y)A(x):Typey : Y \vdash \underset{x : X(y)}{\sum} A(x) : Type
fiberproduct X×f *A = f !f *A =X× YA X f Y\array{ X \times f^* A &=& f_! f^* A & = X \times_Y A\\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y}product type y:YX(y)×A(y):Typey : Y \vdash X(y) \times A(y) : Type
Beck-Chevalley condition of codomain fibrationsubstitution commutes with dependent sum
path space object A I (d 1,d 0) A×A\array{A^I \\ \downarrow^{\mathrlap{(d_1,d_0)}} \\ A \times A}identity type a,b:A(a=b)a,b : A \vdash (a = b)
(-2)-truncated morphism/equivalence Y X\array{Y \\ \downarrow^{\mathrlap{\simeq}} \\ X}true/unit type x:X1:Typex : X \vdash 1 : Type
(-1)-truncated morphism/monomorphism ϕ X\array{\phi \\ \downarrow \\ X}proposition x:Xϕ(x):Typex : X \vdash \phi(x) : Type
direct image of (-1)-truncated morphismuniversal quantifier y:YxX(y)ϕ(x):Typey : Y \vdash \underset{x \in X(y)}{\forall} \phi(x) : Type
(-1)-truncation of postcomposition of (-1)-truncated morphismexistential quantifier y:YxX(y)ϕ(x)y : Y \vdash \underset{x \in X(y)}{\exists} \phi(x)

The symbols in the right column may be formally manipulated according to the rules of type theory. For the case of ordinary categories, this table defines a functor

Lang:LocallyCartesianClosedCategoriesDependentTypeTheories Lang : LocallyCartesianClosedCategories \to DependentTypeTheories

from locally cartesian closed categories to dependent type theories that sends each category to its internal language.

The important fact is that

Theorem

The functor LangLang is an equivalence of categories.

This is discussed at relation between type theory and category theory. So the (dependent) type theory is just an equivalent way of talking about a (locally cartesian closed category).

For the case of (∞,1)-categories/homotopy theories that we are interested in here, there remain some things to be fully worked out, but it is clear that we get an analogous construction

Lang:LocallyCartesianClosed(,1)CategoriesHomotopyTypeTheory Lang : LocallyCartesianClosed(\infty,1)Categories \to HomotopyTypeTheory

from locally cartesian closed (∞,1)-categories to homotopy type theory which is expected to be an equivalence of (∞,1)-categories.

As the above table shows, from the perspective of dependent type theory categories 𝒞\mathcal{C} are regarded systematically via the collection of their slice categories (their associated “hyperdoctrines”). If 𝒞\mathcal{C} is a locally cartesian closed category then every morphism f:XYf : X \to Y in 𝒞\mathcal{C} induces an adjoint triple of functors between the corresponding slice categories

{}

(dependent sum \dashv base change \dashv dependent product) = ( ff * f):𝒞 /X𝒞 /Y(\sum_f \dashv f^* \dashv \prod_f) : \mathcal{C}_{/X} \to \mathcal{C}_{/Y}.

Many familiar constructions are usefully expressed entirely in terms of these adjoint triples. For instance the internal hom in a slice category.

While this is in principle clear/well known, the systematic use of the base change adjoint triple enforced by type theory turns out to lead to various elegant constructions that have not found much attention before, and which can be useful in applications.

Homotopy pullbacks

The yoga of homotopy pullbacks, homotopy fibers, loop space objects, fiber sequences etc. is basic to homotopy theory, and of course is also fairly elementary. Homotopy type theory can hardly add a previously unknown fact here. Nevertheless, it is noteworthy that many of these constructions, elementary as they are, look even simpler when formulated in homotopy type theory.

category theorytype theory
homotopy pullback A× C hB B g A f X\array{A \times_C^h B &\to& B \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{g}} \\ A &\stackrel{f}{\to}& X}a:A,b:B(f(a)=g(b))\underset{a : A, b : B}{\sum} (f(a) = g(b)) / {a:A,b:B;(f(a)=g(b))}\{ a : A, b : B ; (f(a) = g(b)) \}
homotopy fiber hfib(f) * A f X\array{hfib(f) &\to& * \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{}} \\ A &\stackrel{f}{\to}& X} a:A(f(a)=*)\sum_{a : A} (f(a) = *) / {a:A;(f(a)=*)}\{ a : A ; (f(a) = *) \}
mapping cocylinder CoCyl(f) X f Y I d 0 Y d 1 Y\array{ CoCyl(f) &\to& X \\ \downarrow && \downarrow^{\mathrlap{f}} \\ Y^I &\stackrel{d_0}{\to} & Y \\ \downarrow^{\mathrlap{d_1}} \\ Y } y:Yx:X(f(x)=y)y : Y \vdash \underset{x : X}{\sum} (f(x) = y)
free loop space object X X X X×X\array{\mathcal{L}X &\to& X \\ \downarrow &\swArrow_{\simeq}& \downarrow \\ X &\to& X \times X}x,y:X(x=y)and(x=y)\underset{x,y : X}{\sum} (x = y) and (x = y)

Detecting nn-truncation

The central insight (due to Vladimir Voevodsky) that boosts dependent type theory with identity types to genuine homotopy type theory is that in terms of identity types there are simple natural expressions for n-truncation and detection of nn-truncation of objects and morphisms. Translated via categorical semantics to homotopy theory, these formulas turn out to refomulate some basic yoga of model category computation in a new way that hasn’t received attention before in homotopy theory, emphasizing the base change adjoint triple.

category theorytype theory
object XX is (-2)-truncated/contractibleisContr(X)= x:X y:X(x=y)(X) = \sum_{x : X} \prod_{y : X} (x = y)
morphism XX is (-2)-truncated/equivalenceisEquiv(f) x:XisContr(hfiber(f,x)(f) \coloneqq \prod_{x : {X}} isContr(hfiber(f,x)
Remark

In the (∞,1)-category ∞Grpd it is true that a morphism f:XYf : X \to Y is an equivalence precisely if for all global points y:*Yy : * \to Y the corresponding homotopy fiber of ff is contractible. The same simple statement is not available in the “external” logic for a general (∞,1)-category, simply because there an object YY may not even have enough global points (it may be non-trivial and have no global point).

The above is useful in that it says that in the internal logic of the (,1)(\infty,1)-category, the simple statement familiar form ∞Grpd is true generally, after all.

Homotopy algebras over homotopy monads

We have seen that homtopy type theory naturally describes homotopy pullbacks and some other finite (∞,1)-limits in terms of identity types and the base change adjoint triple. The dual notion, homotopy colimits, is conceived of in homotopy type theory as a (vast) generalization of the basic notion of induction and recursion, subsumed type-theoretically in the notion of inductive type, roughly a kind of type that is given by generators and relations.

Traditionally inductive types are in category theory interpreted as algebras over an endofunctor. While useful, this is a concept somewhat alien to usual constructions in category theory or homotopy theory. The natural notion is instead that of an algebra over a monad. While an algebra over an endofunctor may be thought of as a monad-algebra over a free monad, from the point of view of homotopy theory it still seems unnatural to restrict attention to free monads.

However, after generalization to homotopy type theory this is rectified: here the homotopy-theoretic notion of induction turns out to be about ∞-algebras over an (∞,1)-monad, as one would hope, and a higher inductive type is an initial algebras of a presentable (∞,1)-monad.

(…)

Detecting nn-connectedness

category theorytype theory
(-1)-connected object/ inhabited object XXisInhab(X)...isInhab(X) \coloneqq ...
(-1)-connected morphism/ effective epimorphism f:XYf : X \to Y y:YisInhab( x:X(f(x)=y))\prod_{y : Y} isInhab(\sum_{x : X} (f(x) = y))

Homotopy pushouts

category theorytype theory
homotopy pushout C g B f A A C hB\array{ C &\stackrel{g}{\to}& B \\ {}^{\mathllap{f}}\downarrow &\swArrow_{\simeq}& \downarrow \\ A &\to& A \coprod_C^h B}hpushout(ABC:Type)(f:CA)(g:CB):Type{inl:Bhpushout(f,g) inr:Ahpushout(f,g) glue c:C(inl(f(c))=inr(g(c)))hpushout (A B C : Type) (f : C \to A) (g : C \to B) : Type \coloneqq \left\{ \array{inl : B \to hpushout(f,g) \\ inr : A \to hpushout(f,g) \\ glue \prod_{c : C} (inl(f(c)) = inr(g(c)))} \right.

(…)

Constructing nn-truncation

category theorytype theory
(-1)-truncation τ 1()\tau_{-1}(-)supp(X:Type):Type{proj:XsuppX x,y:suppX(x=y)supp(X : Type) : Type \coloneqq \left\{ \array{ proj : X \to supp X \\ \underset{x, y : supp X}{\prod} (x = y) }\right.

Specific HoTT proofs in homotopy theory

We list in the following theorems in homotopy theory together with such proofs of them in terms of homotopy type theory language that are either new (to the best of our knowledge), or else that are at least considerably simpler than earlier proofs with traditional homotopy theory tools.

Essential uniquenes of group units

(…)

Equivalence of notions of stabilizer \infty-groups

(…)

(…)

Revised on November 15, 2012 13:13:52 by Stephan Alexander Spahn (79.227.160.54)