open import 1Lab.Prelude hiding (fibre)

module 1Lab.intro where

Introduction🔗

This page aims to present a first introduction to cubical type theory, from the perspective of a mathematician who has heard about type theory but has no previous familiarity with it. Specifically, the kind of mathematician that we are appealing to is one who is familiar with some of the ideas in category theory and homotopy theory — however, the text also presents the concepts syntactically, in a way that can be read without any prior mathematical knowledge.

Note that whenever code appears, all of the identifiers are hyperlinked to their definitions, which are embedded in articles that describe the concepts involved. For instance, in the code block below, you can click the symbol ≡ to be taken to the page on path types.

_ :  +  ≡ 
_ = refl

For some operations, we use the built-in Agda definitions, which do not have explanations attached. This is the case for the + operation above. However, in any case, those definitions are either built-ins (in which case only the type matters), or defined as functions, in which case the implementation is visible. The most important built-ins for Cubical Agda, and those most likely to lead you to a built-in Agda page, have their own explanations, linked below:

• The 1Lab.Path page explains the primitives I, i0, i1, _∧_, _∨_, ~, PathP, Partial, _[_↦_], and hcomp.

• The 1Lab.Univalence page explains the primitives Glue, glue, unglue.

With that out of the way, the first thing to do is the aforementioned refresher on type theory. If you’re already familiar with type theory, feel free to skip to What’s next?. If you’re not familiar with some of the connections that HoTT has to other areas of mathematics, like higher category theory and topology, I recommend that you read the type theory section anyway!

Type theory🔗

Type theory is a foundational system for mathematics which, in contrast to a set-theoretic foundation like ZFC, formalises mathematical constructions rather than mathematical proofs. That is, instead of specifying which logical deductions are valid, and then giving a set of axioms which characterise the behaviour of mathematical objects, a type-theoretic foundation specifies directly which mathematical constructions are valid.

Formally speaking, it is impossible to construct objects in set theoretic foundations; Rather, one can, by applying the deduction rules of the logical system and appealing to the axioms of the set theory, prove that an object with the desired properties exists. As an example, if we have a way of referring to two objects $x$ and $y\text{,}$ we can prove that there exists a set representing the ordered pair $(x,y)\text{,}$ using the axiom of pairing. Writing quasi-formally, we could even say that this set is constructed using the expression $\{x,\{x,y\}\}\text{,}$ but this is only a notational convenience.

In contrast, a type-theoretic foundational system, such as HoTT (what we use here), specifies directly how to construct mathematical objects, and proving a theorem becomes a special case of constructing an object. To specify what constructions are well-behaved, we sort the mathematical objects into boxes called types. Just like in set theory, the word “set” is a primitive notion, in type theory, the word “type” is a primitive notion. However, we can give an intuitive explanation: “A type is a thing that things can be”. For instance, things can be natural numbers, but things can not be “two” — hence, the natural numbers are a type, but two is not. Formally, a type is specified by giving:

• A formation rule, which tells us which expressions denote valid types at all. For instance, the formation rule for product types tells us that $\mathbb{N}\times \mathbb{N}$ denotes a well-formed type, but “$\mathbb{N}\times \to$” does not. The formation rules also have the duty of preventing us from running into size issues like Russell’s paradox, by constraining the use of universes.

• A handful of introduction rules, which tell us how to piece previously-constructed objects together to form an object of a different type. Sticking with products as an example, if we have previously constructed objects called $a$ and $b\text{,}$ we can construct an ordered pair $(a,b)\text{.}$

  Since the introduction rules are inseparable from their types, it is impossible to construct an object without knowing in which type it lives. If we used the rule which introduces ordered pairs, we know for sure that we built an object of the product type. To specify that an object lives in a certain type, we use the notation $a:A$ — which can be read as “$a$ inhabits $A$”, or “$a$ is a point of $A$”, or “$a$ has type $A$”.

  The notation for stating inhabitation agrees with mathematical parlance in when both make sense. For example, a function from the reals to the reals is commonly introduced with the notation $f:\mathbb{R}\to \mathbb{R}\text{.}$ In type theory, this is made formal as a typing declaration: $f$ is a point of the type of functions $\mathbb{R}\to \mathbb{R}\text{,}$ hence we know that the rules of function types can be used with $f\text{.}$ However, when introducing a more complex object, we’re forced to break into informality and conventional shorthand: “Let G be a group”. In HoTT, we can directly write $G:\mathrm{Group}$¹, which tells us that the rules for the type of groups apply to $G\text{.}$

• A handful of elimination rules, which say how inhabitants of that type can be manipulated. Keeping with the running example, the product type has elimination rules corresponding to projecting either the first or second component of a pair.

  Furthermore, each elimination rule comes with specified behaviour for when it “interacts” with the introduction rules, a process which we generally call reduction. Repeatedly applying these “interactions” tells us how a given construction can have computational behaviour — by performing a delicate dance of elimination and introduction, we can go from $2+2$ to $4\text{.}$

Now that we have an intuitive motivation for the notions of type theory, we can more precisely discuss the structure of formal type theory and how it differs from formal (material) set theory. The first (and perhaps most important) difference is that formal set theory is a “two layered” system, but type theory only has “one layer”. In (for example) ZFC, we have the deductive framework of first-order logic (the “first layer”), and, using the language of that logical system, we assert the axioms of set theory. This remains valid if we switch set theories: For instance, IZF would substitute first-order logic with first-order intuitionistic logic, and remove the assertion that the axiom of choice holds.

In contrast, type theory only has one layer: The layer of types. What in formal set theory would be a deduction in FOL, in type theory becomes the construction of an inhabitant of a certain type, where propositions are identified with certain types as in the table below. Note that up to a first approximation, we can read each type former as denoting a specific set, or as denoting a specific space.

This segues nicely into another difference between type theory and set theory, which concerns the setup of their deductive systems. A deductive system is a specification for how to derive judgements using rules. We can think of the deductive system as a game of sorts, where the judgements are to be thought of as board positions, and the rules specify the valid moves.

In the deductive system of first-order logic, there is only one kind of judgement, stating that a proposition has a proof. If $A$ is a proposition, then the judgement “$A$ has a proof” is written “$⊢A$”. Note that the judgement $⊢A$ is a part of the metatheory, and the proposition $A$ is a part of the theory itself. That is, $⊢A$ is an external notion, and $A$ is an internal notion.

In type theory, the basic judgement is inhabitation, written $⊢a:A\text{.}$ If $A$ is a type that denotes a proposition, then this is analogous to the judgement $⊢A$ of first-order logic, and we refer to $a$ as a witness of $A\text{,}$ or simply as a proof of $A\text{.}$ Even better, if $A$ is a purely logical proposition such that $⊢A$ holds without any appeal to the principle of excluded middle, then there is a term $a$ for which $⊢a:A$ holds in type theory.

When $A$ is being thought of as a collection of things, we might imagine that $a:A$ is analogous to $a\in A\text{.}$ However, this is not the case: While $a\in A$ is a proposition (an internal statement), $a:A$ is a judgement, an external statement. That is, we can not use $a:A$ with the propositional connectives mentioned in the table above — we can not make statements of the form “if it is not the case that $a:A\text{,}$ then $b:B$”. This is the second difference we will mention between set theory and type theory: The proposition $a\in A$ is an internal relation between previously-constructed terms $a$ and $A\text{,}$ but the external judgement $⊢a:A$ is indivisible, and it does not make sense to talk about $a$ without also bringing up that it’s in $A\text{.}$

The third and final difference is the treatment of equality, which is arguably also the most important part of homotopy type theory. In set theory, given sets $a$ and $b\text{,}$ we have a proposition $a=b\text{,}$ which is given meaning by the axiom of extensionality: $a=b$ whenever $a$ and $b$ behave the same with respect to $\in \text{.}$ Correspondingly, in type theory, we have an equality type, written $a{\equiv }_{A}b$ (where $a,b:A\text{),}$ giving us the internal notion of equality. But we also have an external notion of equality, which encodes the aforementioned interactions between introduction and elimination rules. This is written $⊢a=b:A\text{,}$ and it’s meant to indicate that $a$ and $b$ are the same by definition — hence we call it definitional equality.

Since definitional equality is a judgement, it’s also not subject to the internal propositional connectives — we can not prove, disprove, assume or negate it when working inside type theory, for it does not make sense to say “if $a$ and $b$ are equal by definition, then […]”. Correspondingly, in the Agda formalisation, definitional equality is invisible, since it’s represented by the computation rules of the type theory.

In the rest of this section, we will recall the presentation of the most ubiquitous types. The idea is that if you’ve encountered type theory before, then skimming the explanation here should help snap your mind back into focus, while if this is your first time interacting with it, then the content here should be enough for you to understand the rest of the 1lab development.

Functions🔗

If we have two previously-constructed types $A$ and $B\text{,}$ we can form the type of functions from $A$ to $B$, written $A\to B\text{.}$ Often, functions will also be referred to as maps. A function is, intuitively, a rule prescribing how to obtain an inhabitant of $B$ given an inhabitant of $A\text{.}$ In type theory, this is not only an intuition, but rather a definition. This is in contrast with set theory, where functions are defined to be relations satisfying a certain property.

Given a function $f:A\to B\text{,}$ we can apply it to an inhabitant $a:A\text{,}$ resulting in an inhabitant $fa$ of the codomain $B\text{,}$ called the value of $f$ at $a$. For clarity, we sometimes write $f(a)$ for the value of $f$ at $a\text{,}$ but in Agda, the parentheses are not necessary.

The most general form for constructing an inhabitant of $A\to B$ is called lambda abstraction, and it looks like $(\lambda (x:A).e)\text{,}$ though shorthands exist. In this construction, the subexpression $e$ denotes the body of a function definition, and $x$ is the parameter. You can, and should, think of the expression $\lambda x.e$ as being the same as the notation $x\mapsto e$ often used for specifying a map. Indeed, Agda supports definition of functions using a more traditional, “rule-like” notation, as shorthand for using $\lambda$ abstraction. For instance, the following definitions of inhabitants f and g of $\mathrm{Nat}\to \mathrm{Nat}$ are definitionally the same:

module _ where private

  f : Nat → Nat
  f x = x * 
  -- Function definition
  -- with a "rule".

module _ where private

  g : Nat → Nat
  g = λ x → x * 
  -- Function definition
  -- with λ abstraction

In general, we refer to a way of constructing an inhabitant of a type as an introduction rule, and to a way of consuming an inhabitant of a type as an elimination rule. Concisely, the introduction rule for $A\to B$ is $\lambda$ abstraction, and the elimination rule is function application. A general principle of type theory is that whenever an elimination rule “meets” an introduction rule, we must describe how they interact.

In the case of $\lambda \text{-abstraction}$ meeting function application, this interaction is called $\beta \text{-reduction}$², and it tells us how to compute a function application. This is the usual rule for applying functions defined by rules: The value of $(\lambda x.e)e^{\prime }$ is $e\text{,}$ but with $e^{\prime }$ replacing $x$ whenever $x$ appears in $e\text{.}$ Using the notation that you’d find in a typical³ type theory paper, we can concisely state this as:

In addition, function types enjoy a definitional uniqueness rule, which says “any function is a $\lambda$ expression”. Symbolically, this means that if we have $f:A\to B\text{,}$ the terms $f$ and $(\lambda x.fx)$ are equal, definitionally. This is called $\eta \text{-equality,}$ and when applied right-to-left as a reduction rule, $\eta \text{-reduction.}$

Functions of multiple arguments are defined by iterating the unary function type. Since functions are types themselves, we can define functions whose codomain is another function — where we abbreviate $A\to (B\to C)$ by $A\to B\to C\text{.}$ By the uniqueness rule for function types, we have that any inhabitant of this type is going to be of the form $\lambda x.\lambda y.fxy\text{,}$ which we abbreviate by $\lambda xy.fxy\text{.}$ In Agda, we can write this as λ x y → ..., or by mentioning multiple variables in the left-hand side of a rule, as shown below.

module _ where private

  f : Nat → Nat → Nat
  f x y = x +  * y

Universes🔗

Instead of jumping right into the syntactic definition (and motivation) for universes, I’m going to take a longer route, through topos theory and eventually higher topos theory, which gives a meaning explanation for the idea of universes by generalising from a commonly-understood idea: the correspondence between predicates and subsets. Initially, we work entirely in the category of sets, assuming excluded middle for simplicity. Then we pass to an arbitrary elementary topos, and finally to an arbitrary higher topos. If you don’t want to read about categories, click here

First, let’s talk about subsets. I swear I’m going somewhere with this, so bear with me. We know that subsets correspond to predicates, but what even is a subset?

• If we regard sets as material collections of objects, equipped with a membership relation $\in \text{,}$ then $S$ is a subset of $T$ if every element of $S$ is also an element of $T\text{.}$ However, this notion does not carry over directly to structural set theory (where sets are essentially opaque objects of a category satisfying some properties), or indeed to type theory (where there is no membership relation) — but we can salvage it.

  Instead of thinking of a subset directly as a subcollection, we define a subset $S\subseteq T$ to be an injective function $f:S\hookrightarrow T\text{.}$ Note that the emphasis is on the function and not on the index set $S\text{,}$ since we can have many distinct injective functions with the same domains and codomains (exercise: give two distinct subsets of $\mathbb{N}$ with the same domain⁴).

  To see that this definition is a generalisation of the material definition in terms of $\in \text{,}$ we note that any injective function $f:S\hookrightarrow T$ can be restricted to a bijective function $f:S\stackrel{\sim }{\to }\mathrm{im}(f)\text{,}$ by swapping the original codomain for the image of the function. Since the image is a subset of the codomain, we can interpret any injective $f:S\hookrightarrow T$ as expressing a particular way that $S$ can be regarded as a subset of $T\text{.}$

• Alternatively, we can think of a subset as being a predicate on the larger set $T\text{,}$ which holds of a given element $x$ when $x$ is in the subset $S\text{.}$ Rather than directly thinking of a predicate as a formula with a free variable, we think of it as a characteristic function $\chi :T\to \{0,1\}\text{,}$ from which we can recover the subset $S$ as $\{x\in T:\chi (x)=1\}\text{.}$

  This definition works as-is in structural set theory (where the existence of solution sets for equations — called “equalisers” — is assumed), but in a more general setting (one without excluded middle) like an arbitrary elementary topos, or indeed type theory, we would replace the 2-point set $\{0,1\}$ by an object of propositions, normally denoted with $\Omega \text{.}$

These two definitions are both appealing in their own right — the “subsets are injective functions” can be generalised to arbitrary categories, by replacing the notion of “injective function” with “monomorphism”, while “subsets are predicates” is a very clean notion conceptually. Fortunately, it is well-known that these notions coincide; For the purposes of eventually generalising to universes, I’d like to re-explain this correspondence, in a very categorical way.

Consider some sets $A,B$ and an arbitrary function $f:A\to B$ between them. We define the fibre of $f$ over $y$ to be the set $f^{\ast }(y)=\{x\in A:f(x)=y\}\text{,}$ that is, the set of points of the domain that $f$ maps to $y$ — in the context of set theory, this would be referred to as the preimage of $y\text{,}$ but we’re about to generalise beyond sets, so the more “topological” terminology will be useful. We can often characterise properties of $f$ by looking at all of its fibres. What will be useful here is the observation that the fibres of an injective function have at most one element.

More precisely, let $f:A\hookrightarrow B$ be injective, and fix a point $y\in B$ so we can consider the fibre $f^{\ast }(y)$ over y. If we have two inhabitants $a,b\in f^{\ast }(y)\text{,}$ then we know (by the definition of fibre) that $f(a)=y=f(b)\text{,}$ hence by injectivity of $f\text{,}$ we have $a=b$ — if $f^{\ast }(y)$ has any points at all, then it has exactly one. It turns out that having at most one point in every fibre precisely characterises the injective functions: Suppose $f(a)=f(b)\text{;}$ Then we have two inhabitants of $f^{\ast }(f(a))\text{,}$ $a$ and $b\text{,}$ but since we assumed that $f^{\ast }(y)$ has at most one inhabitant for any $y\text{,}$ we have $a=b\text{,}$ so $f$ is injective.

We call a set (type) $X$ with at most one element (at most one point) a subsingleton, since it is a subset of the singleton set (singleton type), or a proposition, since a choice of point $x\in X$ doesn’t give you any more information than merely telling you “$X$ is inhabited” would. Since there is a 1-to-1 correspondence between subsingletons $X$ and propositions “$X$ is inhabited”, the assignment of fibres $y\mapsto f^{\ast }(y)$ defines a predicate ${\chi }_f:B\to \Omega \text{,}$ where we have implicitly translated between a subsingleton and its corresponding proposition.⁵

Conversely, if we have such an assignment $\chi :B\to \Omega \text{,}$ we can make a map into $B$ with subsingleton fibres by carefully choosing the domain. We take the domain to be the disjoint union of the family $\chi \text{,}$ that is, the set ${\sum }_{(x:B)}\chi (x)\text{.}$ The elements of this set can be described, moving closer to type-theoretic language, as pairs $(i,p)$ where $i\in B$ and $p\in \chi (i)$ is a witness that the subset predicate holds of $i\text{.}$

I claim: the map ${\pi }_1:({\sum }_{(x:B)}\chi (x))\to B$ which takes $(i,p)\mapsto i$ has subsingleton fibres. This is because an element of ${\pi }_1^{\ast }(y)$ is described as a pair $(i,q)\text{,}$ and since it’s in the fibre over $y\text{,}$ we have $i=y\text{;}$ Since $\chi$ (by assumption) takes values in subsingletons, concluding that $i=y$ is enough to establish that any two $(i,q)$ and $(i^{\prime },q^{\prime })\in {\pi }_1^{\ast }(y)$ must be equal.

The point of the entire preceding discussion is that the notions of “injections into $B$” and “maps $B\to \Omega$” are equivalent, and, more importantly, this is enough to characterise the object $\Omega$⁶.

Let me break up this paragraph and re-emphasise, since it’ll be the key idea later: A type of propositions is precisely a classifier for maps with propositional fibres.

Since the subobjects of $B$ are defined to be injections $X\to B\text{,}$ and maps $B\to \Omega$ represent these subobjects (in a coherent way), we call $\Omega$ a subobject classifier, following in the tradition of “classifying objects”. A subobject classifier is great to have, because it means you can talk about logical propositions — and, in the presence of functions, predicates — as if they were points of a type.

However, we often want to talk about sets and families of sets as if they were points of a type, instead of just subsets. We could pass to a higher category that has a discrete object classifier — this would be a “type of sets” —, but then the same infelicity would be repeated one dimension higher: we’d have a classifier for “sets”, but our other objects would look like “categories”, and we wouldn’t be able to classify those!

Thus we might hope to find, in addition to a subobject classifier, we could have a general object classifier, an object $\mathrm{Type}$ such that maps $B\to \mathrm{Type}$ correspond to arbitrary maps $A\to B\text{.}$ Let’s specify this notion better using the language of higher category theory:

A subobject classifier is a representing object for the functor $\mathrm{Sub}:{\mathcal{E}}^{\mathrm{op}}\to \mathbf{Sets}$ which takes an object to its poset of subobjects. Since $\mathrm{Sub}(x)$ is a subcategory of $\mathcal{E}/x\text{,}$ restricted to the objects which are (-1)-truncated, an object classifier would be a representing object for $\mathcal{E}/-\text{,}$ the functor which sends an object $X$ to the category of arbitrary “$X\text{-indexed}$ families”, the slice category over $X\text{.}$ If capturing the directed structure isn’t possible, then, at the very least, it should represent $\mathrm{Core}(\mathcal{E}/-)$ — the core of $\mathcal{E}\text{,}$ so that the isomorphisms between families are accurately represented.

However, there is an issue here: there is, a priori, an entire category $\mathcal{E}/x\text{,}$ but only a set ${\mathbf{Hom}}_{\mathcal{E}}(x,U)\text{.}$ Objects in a category can have non-trivial isomorphisms, but there’s no such notion between elements in a set! Let’s suppose that we had such an equivalence, in the context $\mathcal{E}=\mathbf{Sets}\text{,}$ setting aside the size issues for now: we have an object $U$ equipped with an isomorphism $r:\mathbf{Hom}(\ast ,U)\cong \mathbf{Sets}/\ast \cong \mathbf{Sets}\text{.}$ There’s an element $b=r^{-1}(2):U$ classifying the type of booleans, which should have a non-trivial identification $b=b$ corresponding to the involution on $2\text{.}$ However, this is not possible, since a set (by definition) only has trivial identifications.

One might attempt to remedy the issue by looking for an object classifier in a bicategory, where $\mathbf{Hom}(-,U)$ would be a genuine category. However, this didn’t actually fix anything, since we only shifted the issue one level up: we now have an entire bicategory $\mathcal{E}/x\text{,}$ which can’t be classified by the mere category of maps ${\mathbf{Hom}}_{\mathcal{E}}(-,U)\text{!}$

The issue does eventually resolve itself, if we’re very persistent: if we have an $\infty \text{-category}$ $\mathcal{E}\text{,}$ where $\mathbf{Hom}(-,-)$ can be a genuine $\infty \text{-groupoid,}$ then it’s actually perfectly possible for there to be an object $\mathrm{Type}$ with an isomorphism $\mathcal{E}/-\cong \mathbf{Hom}(-,\mathrm{Type})$ — well, at least as long as we restrict ourselves to $\mathrm{Core}(\mathcal{E}/-)\text{.}$ We’ve finally found a setting where object classifiers can exist: $(\infty ,1)\text{-categories!}$

Again, the importance of object classifiers is that they let us talk about arbitrary objects as if they were points of an object $\mathrm{Type}\text{.}$ Specifically, any object $B$ has a name, a map $┌B┐:\ast \to \mathrm{Type}\text{,}$ which represents the unique map $B\to \ast \text{.}$ To make this connection clearer, let’s pass back to a syntactic presentation of type theory, to see what universes look like “from the inside”.

Universes, internally🔗

Inside type theory, object classifiers present themselves as types which contain types, which we call universes. Every type is contained in some universe, but it is not the case that there is a universe containing all types; In fact, if we did have some magical universe ${\mathrm{Type}}_{\infty }:{\mathrm{Type}}_{\infty }\text{,}$ we could reproduce Russell’s paradox, as is done here.

The solution to this is the usual stratification of objects into “sizes”, with the collection of all “small” objects being “large”, and the collection of all “large” objects being “huge”, etc. On the semantic side, a $(\infty ,1)\text{-topos}$ has a sequence of object classifiers for maps with $\kappa \text{-compact}$ fibres, where $\kappa$ is a regular cardinal; Syntactically, this is reflected much more simply as having a tower of universes with ${\mathrm{Type}}_i:{\mathrm{Type}}_{1+i}\text{.}$ So, in Agda, we have:

module _ where private

  _ : Type
  _ = Nat

  _ : Type₁
  _ = Type

In Agda, we do not have automatically that a “small” object can be considered a “large” object. When this is the case, we say that universes are cumulative. Instead, we have an explicit Lifting construction that lets us treat types as being in higher universes:

  _ : Type₂
  _ = Lift (lsuc (lsuc lzero)) Type

To avoid having Lift everywhere, universes are indexed by a (small) type of countable ordinals, called Level, and constructions can be parametrised by the level(s) of types they deal with. The collection of all $\ell \text{-level}$ types is ${\mathrm{Type}}_{\mathrm{lsuc}\ell }\text{,}$ which is itself a type in the next universe up, etc. Since levels are themselves inhabitants of a type, we do in fact have a definable function $\lambda \ell .{\mathrm{Type}}_{\ell }\text{.}$ To avoid further Russellian paradoxes, functions out of Level must be very big, so they live in the “first infinite universe”, ${\mathrm{Type}}_{\omega }\text{.}$ There is another hierarchy of infinite universes, with ${\mathrm{Type}}_{\omega +i}$ inhabiting ${\mathrm{Type}}_{\omega +(1+i)}\text{.}$ To avoid having even more towers of universes, you can’t quantify over the indices $i$ in ${\mathrm{Type}}_{\omega +i}\text{.}$ To summarize, we have:

To represent a collection of types varying over an value of $A\text{,}$ we use a function type into a universe, called a type family for convenience: A type family over $A$ is a function $A\to {\mathrm{Type}}_i\text{,}$ for some choice of level $i\text{.}$ An example of a type family are the finite types, regarded as a family $\mathrm{Fin}:\mathbb{N}\to \mathrm{Type}$ — where $\mathrm{Fin}(n)$ is a type with $n$ elements. Type families are also used to model type constructors, which are familiar to programmers as being the generic types. And finally, if we have a type $B:{\mathrm{Type}}_i\text{,}$ we can consider the constant family at $B\text{,}$ defined to be the function $\lambda (x:A).B\text{.}$

To cap off the correspondence between universes and object classifiers, thus of type families and maps, we have a theorem stating that the space of maps into $B$ is equivalent to the space of type families indexed by $B\text{.}$ As a reminder, you can click on the name Fibration-equiv to be taken to the page where it is defined and explained.

  _ : ∀ {B : Type} → (Σ[ E ∈ Type ] (E → B)) ≃ (B → Type)
  _ = Fibration-equiv

Universes and size issues🔗

Perhaps one of the most famous paradoxes in the history of formal logic, Russell’s paradox reminds us that, for most reasonable kinds of “collection” — be they sets, types, or categories — considering the collection of all collections that do not contain themselves is a road that leads to madness. The standard way of getting around these issues, at least in set-theoretic foundations as applied to category theory, is to refer to such problematic collections as “classes”, and to only axiomatise the sets which are not too big.

In the branches of mathematics that Alexander Grothendieck influenced, a more common approach is to work instead with Grothendieck universes: A Grothendieck universe is a set $\mathcal{U}$ that forms a transitive model of ZF, closed under $\mathcal{U}\text{-small}$ indexed products. The classification of models of ZF implies that any Grothendieck universe $\mathcal{U}$ is equivalent to a segment of the von Neumann universe ${\mathbf{V}}_{\kappa }\text{,}$ where $\kappa$ is a strongly inaccessible cardinal — essentially, an upper bound on the size of the sets in $\mathcal{U}\text{.}$

In traditional mathematical writing, it is common to entirely ignore size issues, save perhaps for an offhand mention of Grothendieck universes (or strongly inaccessible cardinals) within the first few sections. Working in a proof assistant forces us to be honest about the size of our constructions: Correspondingly, we try to be precise in our prose as well. As mentioned above, Agda universes are stratified into a pair of hierarchies ${\mathrm{Type}}_{\kappa }$ and ${\mathrm{Type}}_{\omega +n}\text{,}$ where we’re using $\kappa$ to stand for a variable of Level type. The Level is a built-in type which contains a constant representing $0\text{,}$ is closed under taking successors, and is closed under taking binary maxima.

We refer to structured type (e.g. a category, or a group) as $\kappa \text{-small}$ when its underlying type inhabits the $\kappa \text{th}$ universe; For the specific case of categories, we also use the terminology locally $\kappa \text{-small}$ to refer to the universe in which the family $\mathbf{Hom}(-,-)$ lands. We use subscript Greek letters in prose to index our structures by their universe level. For example, ${\mathbf{Sets}}_{\kappa }$ is the ($(1+\kappa )\text{-small,}$ locally $\kappa \text{-small)}$ category of $\kappa \text{-small}$ sets.

_ : Type
_ = Level

Our policy is to keep the use of universes “as precise as possible”: Definitions are polymorphic over as many levels as they can possibly be, and they are always placed in the smallest universe in which they fit. This is, however, an iterative process: For example, our definition of “sheaf topos” was originally parametrised over 5 levels, but after formalising more desirable properties of topoi, we have found that the definition only really mentions two levels.

Interlude: Basics of paths🔗

Since the treatment of paths is the most important aspect of homotopy type theory, rest assured that we’ll talk about it in more detail later. However, before discussing the dependent sum of a type family, we must discuss the fundamentals of paths, so that the categorical/homotopical connections can be made clear. Before we even get started, though, there is something that needs to be made very clear:

The only conceptualisation of paths that is accurate in all cases is that types are $\infty \text{-groupoids,}$ and hence path spaces are the Hom-$\infty \text{-groupoids}$ given by the structure of each type. However, this understanding is very bulky, and doesn’t actually help understanding paths all that much — so we present a bunch of other analogies, with the caveat that they only hold for some types, or are only one of the many possible interpretations of paths in those types.

The ideas presented below are grouped in blue <details> elements, but not because they aren’t important; You should read all of them.

One benefit that HoTT brings to the table is that it very naturally leads to mixing and matching the interpretations above. For example, the underlying groupoid of a univalent category can just as well be interpreted as a space, mixing interpretations #2 and #3. The spatial interpretation of categories really shines when we pass to higher categories, where the notion of “unique” behaves very badly.

When thinking $n\text{-categorically,}$ even for small values of $n\text{,}$ one must first weaken “unique” to “unique up to unique isomorphism”, and then to something like “unique up to isomorphism, which is unique up to unique invertible 2-cell”. Reasoning spatially, we see that “unique up to isomorphism” really means that there is a contractible space of choices for that object — a notion which is well-behaved at any level of higher categorical complexity.

Every type $A$ has an associated family of path types — to form a path type, we must have two inhabitants of $A$ handy, called the endpoints. The type of paths between $x$ and $y$ in $A$ is written $x{\equiv }_{A}y\text{,}$ where the subscript $A$ is omitted when it can be inferred from context. The name path is meant to evoke the topological idea of path, after which the paths in cubical type theory were modelled. In topology, a path is defined to be a continuous function from the real unit interval $[0,1]\to X\text{,}$ so that we can interpret a path as being a point “continuously varying over time”.

It would be incredibly difficult (and oversized!) to formalise the entire real line and its topology to talk about paths, which are meant to be a fundamental concept in type theory, so we don’t bother! Instead, we look at which properties of the unit interval $[0,1]$ give paths their nice behaviour, and only add those properties to our type theory. The topological interval is contractible, and it has two endpoint inclusions, with domain the one-point space. Those are the properties that characterise it (for defining paths), so those are the properties we keep!

The interval type, $\mathbb{I}\text{,}$ has two introduction rules — but they are so simple that we refer to them as “closed inhabitants” instead. These are written $i0$ and $i1\text{,}$ and they denote the left- and right- hand side of the unit interval. A classic result in the interpretation of constructive mathematics says that any function defined inside type theory is automatically continuous, and so, we define the type $x{\equiv }_{A}y$ to be the type of functions $f:\mathbb{I}\to A\text{,}$ restricted to those where $f(i0)=x$ and $f(i1)=y$ definitionally.

The introduction rule for paths says that if $e:\mathbb{I}\to A\text{,}$ with $e(i0)=x$ and $e(i1)=y$ (those are definitional equalities), then we can treat it as a path $x{\equiv }_{A}y\text{.}$ Conversely, if we have a term $p:x{\equiv }_{A}y\text{,}$ then we can apply it to an argument $i:\mathbb{I}$ to get a term $p(i)$ of type $A\text{.}$ The type of paths satisfies the same reduction rule ($\beta \text{-reduction)}$ as function types, but with an additional rule that says $p(i0)$ is definitionally equal to $x$ (resp. $i1$ and $y\text{),}$ even if $p$ has not reduced to a $\lambda \text{-abstraction.}$

By considering the constant function at a point $x:A\text{,}$ we obtain a term $(\lambda i.x)$ of type $x{\equiv }_{A}x\text{,}$ called the trivial path, and referred to (for historical reasons) as refl, since for the types that are sets, it expresses reflexivity of equality. In the interpretation of types as $\infty \text{-groupoids,}$ refl is the identity morphism. The rest of the groupoid structure is here too! Any path $p:x\equiv y$ has an inverse $p^{-1}:y\equiv x\text{,}$ and for any $p:x{\equiv }_{A}y$ and $q:y{\equiv }_{A}z\text{,}$ there is a composite path $p\bullet q:x{\equiv }_{A}z\text{.}$ There are paths between paths which express the groupoid identities (e.g. $p\bullet p^{-1}\equiv \mathrm{refl}\text{),}$ and those paths satisfy their own identities (up to a path between paths between paths), and so on.

This little introduction to paths was written so that we can make some of the ideas in the following section, about dependent sums, precise. It’s not meant to be a comprehensive treatment of the path type; For that, see the section Paths, in detail later on.

Sums🔗

Recall that in the construction of a map into $B$ from a predicate $\chi :B\to \Omega \text{,}$ we interpreted $\chi$ as a family of sets with at most one element, and then took the disjoint union of that family, written ${\sum }_{(x:B)}\chi (x)\text{,}$ which admits a projection onto $B\text{.}$ That was actually a sneaky introduction of the dependent sum type former, $\sum \text{!}$ Indeed, the short discussion there also made some mention of the introduction rule, but let’s reiterate with more clarity here.

If we have some index type $A:{\mathrm{Type}}_{\ell }\text{,}$ and a family of types $B\to {\mathrm{Type}}_{{\ell }^{\prime }}\text{,}$ then we can form the dependent sum type ${\sum }_{(x:A)}B\text{.}$ When the index is clear from context, we let ourselves omit the variable, and write $\sum B\text{.}$ Since $\sum B$ is a type, it lives in a universe; Since it admits a projection onto $A$ and a projection onto a fibre of $B\text{,}$ it must be a universe bigger than both $\ell$ and ${\ell }^{\prime }\text{,}$ but it need not be any bigger: The dependent sum of $B$ lives in the universe indexed by $\ell \bigsqcup {\ell }^{\prime }\text{.}$

The introduction rule for $\sum B$ says that if you have an $a:A\text{,}$ and a $b:B(a)\text{,}$ then the pair $(a,b)$ inhabits the type $\sum B\text{.}$ Thus the inhabitants of the dependent sum are ordered pairs, but where the second coordinate has a type which depends on the value of the first coordinate. If we take $B$ to be a constant type family, we recover a type of ordered pairs, which we call the product of $A$ and $B\text{,}$ which is notated by $A\times B\text{.}$

For the elimination rules, well, pairs would be rather useless if we couldn’t somehow get out what we put in, right? The first elimination rule says that if we have an inhabitant $e:{\sum }_{(x:A)}B(x)\text{,}$ then we can project out the first component, which is written $e.fst\text{,}$ to get an inhabitant of $A\text{.}$ The computation rule here says that if you project from a pair, you get back what you put in: $(a,b).fst=a\text{.}$

Projecting out the second component is trickier, so we start by considering the special case where we’re projecting from a literal pair. We know that in $(a,b)\text{,}$ the terms have types $a:A$ and $b:B(a)\text{,}$ so in this case, the second projection is $(a,b).snd:B(a)\text{.}$ When we’re not projecting from a literal pair, though, we’re in a bit of a pickle. How do we state the type of the second projection, when we don’t know what the first component is? Well - we generalise. We know that for a pair, $a=(a,b).fst\text{,}$ so that we may replace the aforementioned typing for $.snd$ with the wordy $(a,b).snd:B((a,b).fst)\text{.}$ Now we don’t use any subterms of the pair in the typing judgement, so we can generalise:

A very common application of the dependent sum type is describing types equipped with some structure. Let’s see an example, now turning to Agda so that we may see how the dependent sum is notated in the formalisation. We define a pointed magma structure on a type to be a point of that type, and a binary function on that type. If we let the type vary, then we get a type family of pointed magma structures:

module _ where private

  Pointed-magma-on : Type → Type
  Pointed-magma-on A = A × (A → A → A)

Taking the dependent sum of this family gives us the type of pointed magmas, where inhabitants can be described as triples $(T,i,m)$ where $T:\mathrm{Type}$ is the underlying type, $i:T$ is the distinguished point, and $m:T\to T\to T$ is the binary operation. Note that, to be entirely precise, the pair would have to be written $(T,(i,m))\text{,}$ but since by far the most common of nested pairs is with the nesting on the right, we allow ourselves to omit the inner parentheses in this case.

  Pointed-magma : Type₁
  Pointed-magma = Σ Type Pointed-magma-on

Note that, since we fixed the family to $\mathrm{Type}\to \mathrm{Type}\text{,}$ and recalling that $\mathrm{Type}:{\mathrm{Type}}_1$ are the first two universes, the type of all pointed magmas in $\mathrm{Type}$ lives in the next universe, ${\mathrm{Type}}_1\text{.}$ If the type of all pointed magmas were in $\mathrm{Type}\text{,}$ then we could again reproduce Russell’s paradox.

Just like functions, pairs enjoy a uniqueness principle, which (since coming up with names is very hard), also goes by $\eta \text{-expansion.}$ The rule says that every inhabitant of a $\Sigma \text{-type}$ is definitionally equal to the pairing of its projections: $p=(p.fst,p.snd)\text{.}$ This essentially guarantees us that the inhabitants of a dependent sum type can’t have any “extra stuff” hiding from our projection maps; They are exactly the pairs, no more, and no less.

The dependent sum is a construction that goes by many names. In addition to the ones mentioned below (which are the names people actually use), you could call it the Grothendieck construction, denote it by $\int B\text{,}$ and have a hearty chuckle — if it weren’t for the fact that the Grothendieck construction is generally taken for functors between categories rather than just groupoids.

• $\mathbf{\Sigma }\text{-type}$, named after its shape;

• Disjoint union, since if we take $A$ to be the 2-point type, then the dependent sum $\sum B$ of $B:2\to \mathrm{Type}$ is exactly the disjoint union $B(0)\uplus B(1)\text{;}$

• Thinking homotopically, you can consider a type family $B:A\to \mathrm{Type}$ to be a fibration, since as we shall see later it satisfies the path lifting property; In that sense, $\sum B$ gives the total space, and the actual fibration is the first projection map $x\mapsto x.fst\text{.}$

This last correspondence will be particularly important later, and it inspires much of the terminology we use in HoTT. Since universes are object classifiers, we know that there is an equivalence between type families $F:B\to \mathrm{Type}$ and maps into $B\text{.}$ Dependent sums and paths let us be more precise about this equivalence: We can turn any type family $F:B\to \mathrm{Type}$ into a map $\mathrm{fst}:\sum F\to B\text{,}$ and looking at the fibre of first over a point $y$ recovers $F(y)\text{.}$ We thus blur this distinction a bit and refer to $F(x)$ for some $x:B$ as a fibre of $F\text{,}$ and we say that something happens fibrewise if it happens for each $F(x)\text{.}$

One last thing to mention about $\Sigma \text{-types}$ is that they are the realization of general subsets. This is a special case of the idea of stuff-with-structure, where the structure is merely a witness for the truth of some predicate of the first value. For example, recall that we defined the fibre of $f$ over $y$ as $\{x\in A:f(x)=y\}\text{.}$ In type theory, this is rendered with a $\Sigma \text{-type,}$ as below:

module _ {A B : Type} where private

  fibre : (A → B) → B → Type
  fibre f y = Σ[ x ∈ A ] (f x ≡ y)

Dependent products🔗

Imagine that we have two types, $A$ and $B\text{.}$ For simplicity, they live in the same universe, which can be any universe of our choice. We know that we can consider $B$ to be a constant type family taking indices in $A\text{:}$ $\lambda (x:A).B\text{.}$ Furthermore, we know that the total space of this family is the product type $A\times B\text{,}$ and that it comes equipped with a projection map $\mathrm{fst}:\sum B\to A\text{.}$

Given any function $f:A\to B\text{,}$ we define its graph $\mathrm{graph}(f):A\to A\times B$ to be the function $\lambda x.(x,f(x))\text{,}$ which takes each point of the input space to an ordered pair where the first coordinate is the input, and the second coordinate is the output of $f$ at that input. The graph of a function is special because of its interaction with the projection map $\mathrm{fst}:A\times B\to A\text{.}$ In particular, we can see that $\lambda x.\mathrm{graph}(f).fst$ is the identity function! This property turns out to precisely characterise the functions $A\to A\times B$ which are the graphs of functions $A\to B\text{.}$

By rewriting the equality we noticed above in terms of function composition, we obtain $.fst\circ \mathrm{graph}(f)=\mathrm{id}\text{.}$ A function, like $\mathrm{graph}(f)\text{,}$ which composes on the right with some other function $\mathrm{fst}$ to give the identity function, is called a section of $\mathrm{fst}\text{.}$ This lets us characterise the functions $A\to B$ as the sections of $\mathrm{fst}:A\times B\to A\text{.}$ In this sense, we see that a function $A\to B$ is precisely a choice of values $f(x)\text{,}$ where $f(x)$ is in the fibre over $x$ — in this case, the fibres over all points are $B\text{!}$

Given a map $g:A\to A\times B$ that we know is a section of $\mathrm{fst}\text{,}$ we can recover a function $f:A\to B\text{.}$ Specifically, given a point $x:A\text{,}$ we know that the second projection $g(x).snd$ has type $B$ — so we can simply define $f$ to be $\lambda x.g(x).snd\text{.}$ Since we know that $g$ is a section of $\mathrm{fst}\text{,}$ we conclude that $\mathrm{graph}(f)=g\text{.}$

This idea generalises cleanly from the case where $B$ is just some type, to the case where $B$ is a type family indexed by $A\text{.}$ We define a section of $B$ to be a function $g:A\to \sum B\text{,}$ where $\mathrm{fst}\circ g=\mathrm{id}\text{.}$ Note that this terminology conflates the type family $B$ with the projection map $\sum B\to A\text{,}$ keeping with the trend of identifying type families with fibrations. Generalising the argument from the previous paragraph, we show that a section $g$ gives a rule for assigning a point in $B(x)$ to each point in $x\text{.}$ We again take the second projection of $g(x).snd\text{,}$ but since now $B$ is a type family, this lives in the type $B(g(x).fst)$ — but since we know that $g$ is a section of $\mathrm{fst}\text{,}$ we can correct this to be $B(x)\text{.}$

We would like to package up such a rule into a function $A\to B\text{,}$ but this is not a well-formed type, since $B$ is a type family. Moreover, this would “forget” that $x$ is sent to the fibre $B(x)\text{.}$ Thus, we introduce a new type former, the dependent product type, written ${\prod }_{(x:A)}B(x)$ or more directly $(x:A)\to B(x)\text{.}$ The inhabitants of this type are precisely the sections of $B\text{!}$ More importantly, the introduction, elimination, computation and uniqueness rules of this type are exactly the same as for the function type.

The dependent product type takes on another very important role when universes are involved: Supporting polymorphism. In programming, we say that a function is polymorphic when it works uniformly over many types; Dependent products where the index type is a universe reflect this exactly. For example, using polymorphism, we can write out the types of the first and second projection maps:

module _ where private

  project-first : (A : Type) (B : A → Type) → Σ A B → A
  project-first A B x = x .fst

  project-second : (A : Type) (B : A → Type)
                 → (p : Σ A B) → B (project-first A B p)
  project-second A B x = x .snd

In the logical interpretation, the dependent product type implements the universal quantifier $\forall \text{.}$ For example (keep in mind that in general, we should not read path types as equality), we could read the type $(xy:A)\to x\equiv y$ as the proposition “for all pairs of points $x$ and $y$ of $A\text{,}$ $x$ is equal to $y$”. However, an inhabitant of this type has a much more interesting topological interpretation!

What next?🔗

While the text above was meant to serve as a linearly-structured introduction to the field of homotopy type theory, the rest of the 1Lab is not organised like this. It’s meant to be an explorable presentation of HoTT, where concepts can be accessed in any order, and everything is hyperlinked together. However, we can highlight the following modules as being the “spine” of the development, since everything depends on them, and they’re roughly linearly ordered.

Paths, in detail🔗

open import 1Lab.Path

The module 1Lab.Path develops the theory of path types, filling in the details that were missing in Interlude - Basics of paths above. In particular, the Path module talks about the structure of the interval type $\mathbb{I}\text{,}$ the definition of dependent paths, squares, and the symmetry involution on paths. It then introduce the transport operation, turns a path between types into an equivalence of types.

It also exposits about the structure of types as Kan complices; In particular, the Path module defines and talks about partial elements, which generalise the notion of “horn of a simplex” to any shape of partial cube; Then, it defines extensibility, which exhibits a partial element as being a subshape of some specific cube, and the composition and filling operations, which express that extensibility is preserved along paths. Finally, it introduces the Cartesian coercion operation, which generalises transport.

To reiterate, paths are the most important idea in cubical type theory, so you should definitely read through this module!

Equivalences🔗

The idea of subsingleton type, mentioned in passing in the discussion about universes and expanded upon in the section on dependent products, generalises to give the notion of h-level, which measures how much interesting homotopical information a type has. A h-level that comes up very often is the level of sets, since these are the types where equality behaves like a logical proposition. Due to their importance, we provide a module defining equivalent characterisations of sets.

open import 1Lab.HLevel

Contractible types can be used to give a definition of equivalence that is well-behaved in the context of higher category theory, but it is not the only coherent notion. We also have half-adjoint equivalences and bi-invertible maps. Finally, we have a module that explains why these definitions are needed in place of the simpler notion of “isomorphism”.

open import 1Lab.Equiv
open import 1Lab.Equiv.Biinv
open import 1Lab.Equiv.HalfAdjoint
open import 1Lab.Counterexamples.IsIso

Univalence🔗

open import 1Lab.Univalence

The module 1Lab.Univalence defines and explains the Glue type former, which serves as the Kan structure of the universe. It then concretises this idea by describing how Glue can be used to turn any equivalence into a path between types, which leads to a proof of the univalence principle. After, we prove that the type of equivalences satisfies the same induction principle as the type of paths, and that universes are object classifiers.

open import 1Lab.Univalence.SIP

While univalence guarantees that equivalence of types is equivalent to paths in types, it does not say anything about types-with-structure, like groups or posets. Fortunately, univalence implies the structure identity principle, which characterises the paths in spaces of “structured types” as being homomorphic equivalence.