open import 1Lab.Type module 1Lab.Path where

# The Intervalπ

In HoTT, the inductively-defined identity type gets a new meaning explanation: continuous paths, in a topological sense. The βkey ideaβ of cubical type theory β and thus, Cubical Agda β is that we can take this as a new *definition* of the identity type, where we interpret a Path in a type by a function where the domain is the *interval type*.

##
**Aside**: A brief comment on the meanings of βequal,β βidenticalβ and βidentified,β and how we refer to inhabitants of path types.

Before getting started, itβs worth taking a second to point out the terminology that will be used in this module (and most of the other pages). In intensional type theory, there is both an external notion of βsamenessβ (definitional equality), and an internal notion of βsameness,β which goes by many names: identity type, equality type, propositional equality, path type, etc.^{1}

In this module, we refer to the type `A β‘ B`

as either (the type of) *paths from A to B* or (the type of) *identifications between A and B*, but **never** as βequalities between A and B.β In particular, the HoTT book comments that we may say β$a$ and $b$ are equalβ when the type $a \equiv b$ is inhabited, but in this development we refer this terminology for the case where $a$ and $b$ inhabit a set.

Instead, for general types, we use β$a$ and $b$ are **identical**β or β$a$ and $b$ are **identified**β (or even the wordier, and rather more literal, βthere is a path between $a$ and $b$β). Depending on the type, we might use more specific words: Paths are said to be **homotopic** when theyβre connected by a path-of-paths, and types are said to be **equivalent** when they are connected by a path.

Path : β {β} (A : Type β) β A β A β Type β Path A = PathP (Ξ» i β A)

The type I is meant to represent the (real, closed) unit interval $[0,1]$, the same unit interval used in the topological definition of path. Because the real unit interval has a least and greatest element β 0 and 1 β the interval *type* also has two global inhabitants, i0 and i1. This is where the analogy with the reals breaks down: Thereβs no such thing as `i0.5`

(much less `i1/Ο`

). In reality, the interval type internalises an abstract interval *object*.

Regardless, since all functions definable in type theory are automatically continuous, we can take a path to be any value in the function type `I β A`

. When working with paths, though, itβs useful to mention the endpoints of a path in its type β that is, the values the function takes when applied to `i0`

and to `i1`

. We can βupgradeβ any function `f : I β A`

to a Path, using a definition that looks suspiciously like the identity function:

private to-path : β {β} {A : Type β} β (f : I β A) β Path A (f i0) (f i1) to-path f i = f i refl : β {β} {A : Type β} {x : A} β x β‘ x refl {x = x} = to-path (Ξ» i β x)

The type `Path A x y`

is also written `x β‘ y`

, when `A`

is not important - i.e.Β when it can be inferred from `x`

and `y`

. Under this interpretation, proof that identification is reflexive (i.e.Β that $x = x$) is given by a Path which yields the same element everywhere on `I`

: The function that is constantly $x$.

If we have a Path, we can apply it to a value of the interval type to get an element of the underlying type. When a path is applied to one of the endpoints, the result is the same as declared in its type β even when weβre applying a path we donβt know the definition of.^{2}

module _ {β} {A : Type β} {x y : A} {p : x β‘ y} where private left-endpoint : p i0 β‘ x left-endpoint i = x right-endpoint : p i1 β‘ y right-endpoint i = y

In addition to the two endpoints i0 and i1, the interval has the structure of a De Morgan algebra. All the following equations are respected (definitionally), but they can not be expressed internally as a Path because I is not in Type.^{3}

- $x \land \id{i0} = \id{i0}$, $x \land \id{i1} = x$
- $x \lor \id{i0} = x$, $x \lor \id{i1} = \id{i1}$
- $\neg(x \land y) = \neg x \lor \neg y$
- $\neg\id{i0} = \id{i1}$, $\neg\id{i1} = \id{i0}$, $\neg\neg x = x$
- $\land$ and $\lor$ are both associative, commutative and idempotent, and distribute over eachother.

Note that, in the formalisation, $\neg x$ is written `~ x`

. As a more familiar description, a De Morgan algebra is a Boolean algebra that does not (necessarily) satisfy the law of excluded middle. This is necessary to maintain type safety.

## Raising Dimensionπ

To wit: In cubical type theory, a term in a context with $n$ interval variables expresses a way of mapping an $n$-cube into that type. One very important class of these maps are the $1$-cubes β lines or *paths* β which represent identifications between terms of that type.

Iterating this construction, a term in a context with 2 interval variables represents a square in the type, which can be read as saying that some *paths* (specialising one of the variables to $i0$ or $i1$) in that space are identical: A path between paths, which we call a *homotopy*.

The structural operations on contexts, and the $\land$ and $\lor$ operations on the interval, give a way of extending from $n$-dimensional cubes to $n+k$-dimensional cubes. For instance, if we have a path like the one below, we can extend it to any of a bunch of different squares:

module _ {β} {A : Type β} {a b : A} {p : Path A a b} where

The first thing we can do is introduce another interval variable and ignore it, varying the path over the non-ignored variable. These give us squares where either the top/bottom or left/right faces are the path `p`

, and the other two are refl.

private drop-j : PathP (Ξ» i β p i β‘ p i) refl refl drop-j i j = p i drop-i : PathP (Ξ» i β a β‘ b) p p drop-i i j = p j

These squares can be drawn as below. Take a moment to appreciate how the *types* of drop-j and drop-i specify the *boundary* of the diagram β A `PathP (Ξ» i β p i β‘ p i) refl refl`

corresponds to a square whose top/bottom faces are both `p`

, and whose left/right faces are both refl (by convention). Similarly, `PathP (Ξ» i β a β‘ b) p p`

has refl as top/bottom faces (recall that refl is the constant function regarded as a path), and `p`

as both left/right faces.

The other thing we can do is use one of the binary operators on the interval to get squares called *connections*, where two adjacent faces are `p`

and the other two are refl:

β§-conn : PathP (Ξ» i β a β‘ p i) refl p β§-conn i j = p (i β§ j) β¨-conn : PathP (Ξ» i β p i β‘ b) p refl β¨-conn i j = p (i β¨ j)

These correspond to the following two squares:

Since iterated paths are used *a lot* in homotopy type theory, we introduce a shorthand for 2D non-dependent paths. A Square in a type is exactly what it says on the tin: a square.

Square : β {β} {A : Type β} {a00 a01 a10 a11 : A} β (p : a00 β‘ a01) β (q : a00 β‘ a10) β (s : a01 β‘ a11) β (r : a10 β‘ a11) β Type β Square p q s r = PathP (Ξ» i β p i β‘ r i) q s

The arguments to Square are as in the following diagram, listed in the order βPQSR.β This order is a bit unusual (itβs one off from being alphabetical, for instance) but it does have a significant benefit: If you imagine that the letters are laid out in a circle, *identical paths are adjacent*. Reading the square in the left-right direction, it says that $p$ and $r$ are identical β these are adjacent if you βfold upβ the sequence `p q s r`

. Similarly, reading top-down, it says that $q$ and $s$ are identical - these are directly adjacent.

## Symmetryπ

The involution `~_`

on the interval type gives a way of inverting paths β a proof that identification is symmetric.

sym : β {ββ} {A : Type ββ} {x y : A} β x β‘ y β y β‘ x sym p i = p (~ i)

As a minor improvement over βBook HoTT,β this operation is *definitionally* involutive:

module _ {β} {A : Type β} {x y : A} {p : x β‘ y} where private sym-invol : sym (sym p) β‘ p sym-invol i = p

# Pathsπ

While the basic structure of the path type is inherited from its nature as functions out of an internal De Morgan algebra, the structure of *identifications* presented by paths is more complicated. For starters, letβs see how paths correspond to identifications in that they witness the logical principle of βindiscernibility of identicals.β

## Transportπ

A basic principle of identity is that *identicals are indiscernible*: if $x = y$ and $P(x)$ holds, then $P(y)$ also holds, for any choice of predicate $P$. In type theory, this is generalised, as $P$ can be not only a predicate, but any type family.

The way this is incarnated is by an operation called transport, which says that every path between `A`

and `B`

gives rise to a *function* `A β B`

.

transport : β {β} {A B : Type β} β A β‘ B β A β B transport p = transp (Ξ» i β p i) i0

The transport operation is the earliest case of when thinking of `p : A β‘ B`

as merely saying βA and B are equalβ goes seriously wrong. A path gives a *specific* identification of `A`

and `B`

, which can be highly non-trivial.

As a concrete example, it can be shown that the type `Bool β‘ Bool`

has exactly two inhabitants (see here), which is something like saying βthe set of booleans is equal to itself in two ways.β That phrase is nonsensical, which is why βthere are two paths Bool β Boolβ is preferred: itβs not nonsense.

In Cubical Agda, transport is a derived notion, with the actual primitive being transp. Unlike transport, which has two arguments (the path, and the point to transport), `transp`

has *three*:

The first argument to transp is a

*line*of types, i.e.Β a function`A : I β Type`

, just as for transport.The second argument to transp has type I, but itβs not playing the role of an endpoint of the interval. Itβs playing the role of a

*formula*, which specifies*where the transport is constant*: In`transp P i1`

,`P`

is required to be constant, and the transport is the identity function:_ : β {β} {A : Type β} β transp (Ξ» i β A) i1 β‘ id _ = refl

The third argument is an inhabitant of

`A i0`

, as for transport.

This second argument, which lets us control where transp is constant, brings a lot of power to the table! For example, the proof that transporting along refl is `id`

is as follows:

transport-refl : β {β} {A : Type β} (x : A) β transport (Ξ» i β A) x β‘ x transport-refl {A = A} x i = transp (Ξ» _ β A) i x

Since `Ξ» i β A`

is a constant function, the definition of transport-refl is well-typed, and it has the stated endpoints because transport is defined to be `transp P i0`

, and `transp P i1`

is the identity function.

In fact, this generalises to something called the *filler* of transport: `transport p x`

and `x`

*are* identical, but theyβre identical *over* the given path:

transport-filler : β {β} {A B : Type β} β (p : A β‘ B) (x : A) β PathP (Ξ» i β p i) x (transport p x) transport-filler p x i = transp (Ξ» j β p (i β§ j)) (~ i) x

## We also have some special cases of transport-filler which are very convenient when working with iterated transports.

transport-filler-ext : β {β} {A B : Type β} (p : A β‘ B) β PathP (Ξ» i β A β p i) (Ξ» x β x) (transport p) transport-filler-ext p i x = transport-filler p x i transportβ»-filler-ext : β {β} {A B : Type β} (p : A β‘ B) β PathP (Ξ» i β p i β A) (Ξ» x β x) (transport (sym p)) transportβ»-filler-ext p i x = transp (Ξ» j β p (i β§ ~ j)) (~ i) x transportβ»transport : β {β} {A B : Type β} (p : A β‘ B) (a : A) β transport (sym p) (transport p a) β‘ a transportβ»transport p a i = transportβ»-filler-ext p (~ i) (transport-filler-ext p (~ i) a)

The path is constant when `i = i0`

because `(Ξ» j β p (i0 β§ j))`

is `(Ξ» j β p i0)`

(by the reduction rules for `_β§_`

). It has the stated endpoints, again, because `transp P i1`

is the identity function.

By altering a path `p`

using a predicate `P`

, we get the promised principle of *indiscernibility of identicals*:

subst : β {ββ ββ} {A : Type ββ} (P : A β Type ββ) {x y : A} β x β‘ y β P x β P y subst P p x = transp (Ξ» i β P (p i)) i0 x

### Computationπ

In βBook HoTT,β transport is defined using path induction, and it computes definitionally on refl. We have already seen that this is not definitional in cubical type theory, which might lead you to ask: When does transport compute? The answer is: By cases on the path. The structure of the path `P`

is what guides reduction of transport. Here are some reductions:

For the natural numbers, and other inductive types without parameters, transport is always the identity function. This is justified because thereβs nothing to vary in Nat, so we can just ignore the transport:

_ : {x : Nat} β transport (Ξ» i β Nat) x β‘ x _ = refl

For other type formers, the definition is a bit more involved. Letβs assume that we have two lines, `A`

and `B`

, to see how transport reduces in types built out of `A`

and `B`

:

module _ {A : I β Type} {B : I β Type} where private

For non-dependent products, the reduction rule says that βtransport is homomorphic over forming productsβ:

_ : {x : A i0} {y : B i0} β transport (Ξ» i β A i Γ B i) (x , y) β‘ (transport (Ξ» i β A i) x , transport (Ξ» i β B i) y) _ = refl

For non-dependent functions, we have a similar situation, except one the transports is *backwards*. This is because, given an `f : A i0 β B i0`

, we have to turn an `A i1`

into an `A i0`

to apply f!

_ : {f : A i0 β B i0} β transport (Ξ» i β A i β B i) f β‘ Ξ» x β transport (Ξ» i β B i) (f (transport (Ξ» i β A (~ i)) x)) _ = refl module _ {A : I β Type} {B : (i : I) β A i β Type} where private

In the dependent cases, we have slightly more work to do. Suppose that we have a line `A : I β Type β`

and a *dependent* line `B : (i : I) β A i β Type β`

. Letβs characterise transport in the lines `(Ξ» i β (x : A i) β B i x)`

. A first attempt would be to repeat the non-dependent construction: Given an `f : (x : A i0) β B i0 x`

and an argument `x : A i1`

, we first get `x' : A i0`

by transporting along `Ξ» i β A (~ i)`

, compute `f x' : B i0 x`

, then transport along `(Ξ» i β B i x')`

to g- Wait.

_ : {f : (x : A i0) β B i0 x} β transport (Ξ» i β (x : A i) β B i x) f β‘ Ξ» (x : A i1) β let x' : A i0 x' = transport (Ξ» i β A (~ i)) x

We canβt βtransport along `(Ξ» i β B i x')`

,β thatβs not even a well-formed type! Indeed, `B i : A i β Type`

, but `x' : A i1`

. What we need is some way of connecting our original `x`

and `x'`

, so that we may get a `B i1 x'`

. This is where transport-filler comes in:

xβ‘x' : PathP (Ξ» i β A (~ i)) x x' xβ‘x' = transport-filler (Ξ» i β A (~ i)) x

By using `Ξ» i β B i (xβ‘x' (~ i))`

as our path, we a) get something type-correct, and b) get something with the right endpoints. `(Ξ» i β B i (xβ‘x' (~ i)))`

connects `B i0 x`

and `B i1 x'`

, which is what we wanted.

fx' : B i0 x' fx' = f x' in transport (Ξ» i β B i (xβ‘x' (~ i))) fx' _ = refl

The case for dependent products (i.e.Β general Ξ£ types) is analogous, but without any inverse transports.

## Path Inductionπ

The path induction principle, also known as βaxiom J,β essentially breaks down as the following two statements:

Identicals are indiscernible (transport)

Singletons are contractible. The type

`Singleton A x`

is the βsubtype of A of the elements identical to xβ:

Singleton : β {β} {A : Type β} β A β Type _ Singleton x = Ξ£[ y β _ ] (x β‘ y)

There is a canonical inhabitant of `Singleton x`

, namely `(x, refl)`

. To say that `singletons`

are contractible is to say that every other inhabitant has a path to `(x, refl)`

:

Singleton-is-contr : β {β} {A : Type β} {x : A} (y : Singleton x) β Path (Singleton x) (x , refl) y Singleton-is-contr {x = x} (y , path) i = path i , square i where square : Square refl refl path path square i j = path (i β§ j)

Thus, the definition of J: transport + Singleton-is-contr.

J : β {ββ ββ} {A : Type ββ} {x : A} (P : (y : A) β x β‘ y β Type ββ) β P x refl β {y : A} (p : x β‘ y) β P y p J {x = x} P prefl {y} p = transport (Ξ» i β P (path i .fst) (path i .snd)) prefl where path : (x , refl) β‘ (y , p) path = Singleton-is-contr (y , p)

This eliminator *doesnβt* definitionally compute to `prefl`

when `p`

is `refl`

, again since `transport (Ξ» i β A)`

isnβt definitionally the identity. However, since it *is* a transport, we can use the transport-filler to get a path expressing the computation rule.

J-refl : β {ββ ββ} {A : Type ββ} {x : A} (P : (y : A) β x β‘ y β Type ββ) β (pxr : P x refl) β J P pxr refl β‘ pxr J-refl {x = x} P prefl i = transport-filler (Ξ» i β P _ (Ξ» j β x)) prefl (~ i)

## Functorial Actionπ

In HoTT, every function behaves like a funct**or**, in that it has an action on objects (the actual computational content of the function) and an action on *morphisms* β how that function acts on paths. Reading paths as identity, this is a proof that functions take identical inputs to identical outputs.

ap : β {a b} {A : Type a} {B : A β Type b} (f : (x : A) β B x) {x y : A} β (p : x β‘ y) β PathP (Ξ» i β B (p i)) (f x) (f y) ap f p i = f (p i)

The following function expresses the same thing as ap, but for binary functions. The type is huge! Thatβs because it applies to the most general type of 2-argument dependent function possible: `(x : A) (y : B x) β C x y`

. Even then, the proof is beautifully short:

apβ : β {a b c} {A : Type a} {B : A β Type b} {C : (x : A) β B x β Type c} (f : (x : A) (y : B x) β C x y) {x y : A} {Ξ± : B x} {Ξ² : B y} β (p : x β‘ y) β (q : PathP (Ξ» i β B (p i)) Ξ± Ξ²) β PathP (Ξ» i β C (p i) (q i)) (f x Ξ±) (f y Ξ²) apβ f p q i = f (p i) (q i)

This operation satisfies many identities definitionally that are only propositional when ap is defined in terms of J. For instance:

module _ {A B C : Type} {f : A β B} {g : B β C} where ap-comp : {x y : A} {p : x β‘ y} β ap (Ξ» x β g (f x)) p β‘ ap g (ap f p) ap-comp = refl ap-id : {x y : A} {p : x β‘ y} β ap (Ξ» x β x) p β‘ p ap-id = refl ap-sym : {x y : A} {p : x β‘ y} β sym (ap f p) β‘ ap f (sym p) ap-sym = refl ap-refl : {x : A} β ap f (Ξ» i β x) β‘ (Ξ» i β f x) ap-refl = refl

The last lemma, that `ap`

respects composition of *paths*, needs path induction, and the rest of the groupoid structure on type formers, so itβs in a different module.

# Compositionπ

In βBook HoTT,β the primitive operation from which the higher-dimensional structure of types is derived is the J eliminator, with J-refl as a *definitional* computation rule. This has the benefit of being very elegant: This one elimination rule generates an infinite amount of coherent data. However, itβs very hard to make compute in the presence of higher inductive types and univalence, so much so that, in the book, univalence and HITs only compute up to paths.

In Cubical Agda, types are interpreted as objects called *cubical Kan complexes*^{4}, which are a *geometric* description description of spaces as βsets we can probe by cubes.β In Agda, this βprobingβ is reflected by mapping the interval into a type: A βprobeβ of $A$ by an $n$-cube is a term of type $A$ in a context with $n$ variables of type I β points, lines, squares, cubes, etc. This structure lets us βexploreβ the higher dimensional structure of a type, but it does not specify how this structure behaves.

Thatβs where the βKanβ part of βcubical Kan complexβ comes in: Semantically, *every open box extends to a cube*. The concept of βopen boxβ might make even less sense than the concept of βcube in a typeβ initially, so it helps to picture them! Suppose we have three paths $p : w β‘ x$, $q : x β‘ y$, and $r : y β‘ z$. We can pictorially arrange them into an open box like in the diagram below, by joining the paths by their common endpoints:

In the diagram above, we have a square assembled of three lines $w β‘ x$, $x β‘ y$, and $y β‘ z$. Note that in the left face of the diagram, the path was inverted; This is because while we have a path $w β‘ x$, we need a path $x β‘ w$, and all parallel faces of a cube must βpointβ in the same direction. The way the diagram is drawn strongly implies that there is a face missing β the line $w β‘ z$. The interpretation of types as *Kan* cubical sets guarantees that the open box above extends to a complete square, and thus the line $w β‘ z$ exists.

## Partial Elementsπ

The definition of Kan cubical sets as those having fillers for all open boxes is all well and good, but to use this from within type theory we need a way of reflecting the idea of βopen boxβ as syntax. This is done is by using the Partial type former.

The Partial type former takes two arguments: A *formula* $\varphi$, and a *type* $A$. The idea is that a term of type $\id{Partial}\ \varphi\ A$ in a context with $n$ I-typed variables is a $n$-cube that is only defined when $\varphi$ βis true.β In Agda, formulas are represented using the De Morgan structure of the interval, and they are βtrueβ when they are equal to 1. The predicate `IsOne`

represents truth of a formula, and there is a canonical inhabitant 1=1 which says i1 is i1.

For instance, if we have a variable `i : I`

of interval type, we can represent *disjoint endpoints* of a Path by a partial element with formula $\neg i \lor i$. Note that this is not the same thing as i1! Since elements of `I`

are meant to represent real numbers $r \in [0,1]$, it suffices to find one for which $\max(x, 1 - x)$ is not $1$ β like 0.5.

private not-a-path : (i : I) β Partial (~ i β¨ i) Bool not-a-path i (i = i0) = true not-a-path i (i = i1) = false

This represents the following shape: Two disconnected points, with completely unrelated values at each endpoint of the interval.

More concretely, an element of Partial can be understood as a function where the domain is the predicate `IsOne`

, which has an inhabitant 1=1, stating that one is one. Indeed, we can *apply* a Partial to an argument of type `IsOne`

to get a value of the underlying type.

_ : not-a-path i0 1=1 β‘ true _ = refl

Note that if we *did* have `(~i β¨ i) = i1`

(i.e.Β our De Morgan algebra was a Boolean algebra), the partial element above would give us a contradiction, since any `I β Partial i1 T`

extends to a path:

_ : (f : I β Partial i1 Bool) β Path Bool (f i0 1=1) (f i1 1=1) _ = Ξ» f i β f i 1=1

## Extensibilityπ

A partial element in a context with $n$-variables gives us a way of mapping some subobject of the $n$-cube into a type. A natural question to ask, then, is: Given a partial element $e$ of $A$, can we extend that to a honest-to-god *element* of $A$, which agrees with $e$ where it is defined?

Specifically, when this is the case, we say that $x : A$ *extends* $e : \id{Partial}\ \varphi\ A$. We could represent this very generically as a *lifting problem*, i.e.Β trying to find a map $\square^n$ which agrees with $e$ when restricted to $\varphi$, but I believe a specific example will be more helpful.

Suppose we have a partial element of Bool which is true on the left endpoint of the interval, and undefined elsewhere. This is a partial element with one interval variable, so it would be extended by a *path* β a 1-dimensional cube. The reflexivity path is a line in `Bool`

, which is true on the left endpoint of the interval (in fact, it is true everywhere), so we say that refl *extends* the partial element.

In the diagram, we draw the specific partial element being extended in red, and the total path extending it in black. In Agda, extensions are represented by the type former Sub, which we abbreviate by _[_β¦_]. Fully applied, that operator looks like `A [ Ο β u ]`

.^{5}

_[_β¦_] : β {β} (A : Type β) (Ο : I) (u : Partial Ο A) β _ A [ Ο β¦ u ] = Sub A Ο u

We can formalise the red-black extensibility diagram above by defining the partial element left-true and giving refl to inS, the constructor for _[_β¦_].

private left-true : (i : I) β Partial (~ i) Bool left-true i (i = i0) = true refl-extends : (i : I) β Bool [ (~ i) β¦ left-true i ] refl-extends i = inS (refl {x = true} i)

The constructor `inS`

expresses that *any* totally-defined cube $u$ can be seen as a partial cube, one that agrees with $u$ for any choice of formula $\varphi$. This might be a bit abstract, so letβs diagram the case where we have some square $a$, and the partial element has formula $i \land j$. This extension can be drawn as in the diagram below: The red βbackwards Lβ shape is the partial element, which is βextended byβ the black lines to make a complete square.

_ : β {β} {A : Type β} {Ο : I} (u : A) β A [ Ο β¦ (Ξ» _ β u) ] _ = inS

Note that since an extension must agree with the partial element *everywhere*, there are elements that can not be extended at all. Take `notAPath`

from before β since there is no path that is true at i0 and false at i1, it is not extensible. If it were extensible, we would have `true β‘ false`

β a contradiction.^{6}

not-extensible : ((i : I) β Bool [ (~ i β¨ i) β¦ not-a-path i ]) β true β‘ false not-extensible ext i = outS (ext i)

This counterexample demonstrates the eliminator for _[_β¦_], outS, which turns an `A [ Ο β¦ u ]`

to `A`

, with a computation rule saying that, for `x : A [ i1 β¦ u ]`

, `outS x`

computes to `u 1=1`

:

_ : β {A : Type} {u : Partial i1 A} {x : A [ i1 β¦ u ]} β outS x β‘ u 1=1 _ = refl

The notion of partial elements and extensibility captures the specific interface of the Kan operations, which can be summed up in the following sentence: *If a partial path is extensible at i0, then it is extensible at i1*. Letβs unpack that a bit:

A *partial path* is anything of type `I β Partial Ο A`

β letβs say we have an `f`

in that type. It takes a value at i0 (thatβs `f i0`

), and a value at i1. The Kan condition expresses that, if there exists an `A [ Ο β f i0 ]`

, then we also have an `A [ Ο β f i1 ]`

. In other words: Extensibility is preserved by paths.

Recall the open box we drew by gluing paths together at the start of the section (on the left). It has a *top face* `q`

, and it has a *tube* β its left/right faces, which can be considered as a partial (in the left-right direction) path going in the top-down direction.

We can make this the construction of this βtubeβ formal by giving a Partial element of `A`

, which is defined on $\neg i \lor i$ (that is: only the left/right faces of a square), as is done below. Since it is a tube of a *square*, it has *two* interval variables: $j$ gives the top-down direction.^{7}

module _ {A : Type} {w x y z : A} {p : w β‘ x} {q : x β‘ y} {r : y β‘ z} where private double-comp-tube : (i : I) β I β Partial (~ i β¨ i) A double-comp-tube i j (i = i0) = sym p j double-comp-tube i j (i = i1) = r j

When given i0 as `j`

, double-comp-tube has boundary $p\ \id{i1} \to r\ \id{i0}$, which computes to $x \to y$. This means that for this path to be extensible at i0, we need a path with that boundary. By assumption, `q`

extends double-comp-tube at i0.

extensible-at-i0 : (i : I) β A [ (i β¨ ~ i) β¦ double-comp-tube i i0 ] extensible-at-i0 i = inS (q i)

We can draw this as one of our red-black extensibility diagrams colouring the left/right faces in red β since that is the partial element β and colouring the top face black, since that is a totally-defined cube.

The Kan condition says that this path is then extensible at `i1`

, i.e. there is some inhabitant of `A [ (i β¨ ~ i) β¦ double-comp-tube i i1 ]`

. This element is written using the operator hcomp:

extensible-at-i1 : (i : I) β A [ (i β¨ ~ i) β¦ double-comp-tube i i1 ] extensible-at-i1 i = inS (hcomp {Ο = ~ i β¨ i} (Ξ» k is1 β double-comp-tube i k is1) (q i))

Unwinding what it means for this element to exist, we see that the hcomp operation guarantees the existence of a path $w \to z$. It is the face that is hinted at by completing the open box above to a complete square.

double-comp : w β‘ z double-comp i = outS (extensible-at-i1 i)

Note that hcomp gives us the missing face of the open box, but the semantics guarantees the existence of the box itself, as a $n$-cube. From the De Morgan structure on the interval, we can derive the existence of the cubes themselves (called **fillers**) from the existence of the missing faces:

hfill : β {β} {A : Type β} {Ο : I} (u : I β Partial Ο A) (u0 : A [ Ο β¦ u i0 ]) β outS u0 β‘ hcomp u (outS u0) hfill {Ο = Ο} u u0 i = hcomp (Ξ» j β Ξ» { (Ο = i1) β u (i β§ j) 1=1 ; (i = i0) β outS u0 }) (outS u0)

**Note**: While every inhabitant of Type has a composition operation, not every *type* (something that can be on the right of type signature `e : T`

) does. We call the types that *do* have a composition operation βfibrant,β since these are semantically the cubical sets which are Kan complices. Examples of types which are *not* fibrant include the interval I, the partial elements Partial, and the extensions `_[_β¦_]`

^{8}.

Definition: A type isfibrantif it supports hcomp. This word comes up a lot when discussing not only the semantics of Cubical type theory, but also its practice! For instance, the fibrancy of Type is what powers univalence.

Agda also provides a *heterogeneous* version of composition (also called CCHM composition), called comp. It too has a corresponding filler, called fill. The idea behind CCHM composition is β by analogy with hcomp expressing that βpaths preserve extensibilityβ β that PathPs preserve extensibility. Thus we have:

private comp-verbose : β {β} (A : I β Type β) {Ο : I} β (u : β i β Partial Ο (A i)) β (u0 : A i0 [ Ο β¦ u i0 ] ) β A i1 [ Ο β¦ u i1 ] comp-verbose A u u0 = inS (comp A u (outS u0)) fill : β {β : I β Level} (A : β i β Type (β i)) {Ο : I} β (u : β i β Partial Ο (A i)) β (u0 : A i0 [ Ο β¦ u i0 ]) β β i β A i fill A {Ο = Ο} u u0 i = comp (Ξ» j β A (i β§ j)) (Ξ» j β Ξ» { (Ο = i1) β u (i β§ j) 1=1 ; (i = i0) β outS u0 }) (outS u0)

Given the inputs to a composition β a family of partial paths `u`

and a base `u0`

β hfill connects the input of the composition (`u0`

) and the output. The cubical shape of iterated identifications causes a slight oddity: The only unbiased definition of path composition we can give is *double composition*, which corresponds to the missing face for the square at the start of this section.

_Β·Β·_Β·Β·_ : β {β} {A : Type β} {w x y z : A} β w β‘ x β x β‘ y β y β‘ z β w β‘ z (p Β·Β· q Β·Β· r) i = hcomp (Ξ» j β Ξ» { (i = i0) β p (~ j) ; (i = i1) β r j }) (q i)

Since it will be useful later, we also give an explicit name for the filler of the double composition square.

Β·Β·-filler : β {β} {A : Type β} {w x y z : A} β (p : w β‘ x) (q : x β‘ y) (r : y β‘ z) β Square (sym p) q (p Β·Β· q Β·Β· r) r Β·Β·-filler p q r i j = hfill (Ξ» k β Ξ» { (j = i0) β p (~ k) ; (j = i1) β r k }) (inS (q j)) i

We can define the ordinary, single composition by taking `p = refl`

, as is done below. The square associated with the binary composition operation is obtained as the same open box at the start of the section, the same double-comp-tube, but by setting any of the faces to be reflexivity. For definiteness, we chose the left face:

_β_ : β {β} {A : Type β} {x y z : A} β x β‘ y β y β‘ z β x β‘ z p β q = refl Β·Β· p Β·Β· q

The ordinary, βsingle compositeβ of $p$ and $q$ is the dashed face in the diagram above. Since we bound Β·Β·-filler above, and defined _β_ in terms of _Β·Β·_Β·Β·_, we can reuse the latterβs filler to get one for the former:

β-filler : β {β} {A : Type β} {x y z : A} β (p : x β‘ y) (q : y β‘ z) β Square refl p (p β q) q β-filler {x = x} {y} {z} p q = Β·Β·-filler refl p q

The single composition has a filler βin the other direction,β which connects $q$ and $p \bullet q$. This is, essentially, because the choice of setting the left face to refl was completely arbitrary in the definition of _β_: we could just as well have gone with setting the *right* face to refl.

β-filler' : β {β} {A : Type β} {x y z : A} β (p : x β‘ y) (q : y β‘ z) β Square (sym p) q (p β q) refl β-filler' {x = x} {y} {z} p q j i = hcomp (Ξ» k β Ξ» { (i = i0) β p (~ j) ; (i = i1) β q k ; (j = i0) β q (i β§ k) }) (p (i β¨ ~ j))

## Uniquenessπ

A common characteristic of *geometric* interpretations of higher categories β like the one we have here β when compared to algebraic definitions is that there is no prescription in general for how to find composites of morphisms. Instead, we have that each triple of morphism has a *contractible space* of composites. We call the proof of this fact Β·Β·-unique:

Β·Β·-unique : β {β} {A : Type β} {w x y z : A} β (p : w β‘ x) (q : x β‘ y) (r : y β‘ z) β (Ξ± Ξ² : Ξ£[ s β (w β‘ z) ] Square (sym p) q s r) β Ξ± β‘ Ξ²

Note that the type of `Ξ±`

and `Ξ²`

asks for a path `w β‘ z`

which *specifically* completes the open box for double composition. We would not in general expect that `w β‘ z`

is contractible for an arbitrary `a`

! Note that the proof of this involves filling a cube in a context that *already* has an interval variable in scope - a hypercube!

Β·Β·-unique {w = w} {x} {y} {z} p q r (Ξ± , Ξ±-fill) (Ξ² , Ξ²-fill) = Ξ» i β (Ξ» j β square i j) , (Ξ» j k β cube i j k) where cube : (i j : I) β p (~ j) β‘ r j cube i j k = hfill (Ξ» l β Ξ» { (i = i0) β Ξ±-fill l k ; (i = i1) β Ξ²-fill l k ; (k = i0) β p (~ l) ; (k = i1) β r l }) (inS (q k)) j square : Ξ± β‘ Ξ² square i j = cube i i1 j

The term `cube`

above has the following cube as a boundary. Since it is a filler, there is a missing face at the bottom which has no name, so we denote it by `hcomp...`

in the diagram.

This diagram is quite busy because it is a 3D commutative diagram, but it could be busier: all of the unimportant edges were not annotated. By the way, the lavender face (including the lavender $p\ \neg j$) is the $k = \id{i0}$ face, and the red face is the $k = \id{i1}$ face.

However, even though the diagram is very busy, most of the detail it contains can be ignored. Reading it in the left-right direction, it expresses an identification between `Ξ±-filler j k`

and `Ξ²-filler j k`

, lying over a homotopy `Ξ± = Ξ²`

. That homotopy is what you get when you read the bottom square of the diagram in the left-right direction. Explicitly, here is that bottom square:

Note that, exceptionally, this diagram is drawn with the left/right edges going up rather than down. This is to match the direction of the 3D diagram above. The colours are also matching.

Readers who are already familiar with the notion of h-level will have noticed that the proof Β·Β·-unique expresses that the type of double composites `p Β·Β· q Β·Β· r`

is a *proposition*, not that it is contractible. However, since it is inhabited (by _Β·Β·_Β·Β·_ and its filler), it is contractible:

Β·Β·-contract : β {β} {A : Type β} {w x y z : A} β (p : w β‘ x) (q : x β‘ y) (r : y β‘ z) β (Ξ² : Ξ£[ s β (w β‘ z) ] Square (sym p) q s r) β (p Β·Β· q Β·Β· r , Β·Β·-filler p q r) β‘ Ξ² Β·Β·-contract p q r Ξ² = Β·Β·-unique p q r _ Ξ²

## Syntax Sugarπ

When constructing long chains of identifications, itβs rather helpful to be able to visualise *what* is being identified with more βpriorityβ than *how* it is being identified. For this, a handful of combinators with weird names are defined:

β‘β¨β©-syntax : β {β} {A : Type β} (x : A) {y z} β y β‘ z β x β‘ y β x β‘ z β‘β¨β©-syntax x q p = p β q infixr 2 β‘β¨β©-syntax syntax β‘β¨β©-syntax x q p = x β‘β¨ p β© q _β‘Λβ¨_β©_ : β {β} {A : Type β} (x : A) {y z : A} β y β‘ x β y β‘ z β x β‘ z x β‘Λβ¨ p β©β‘Λ q = (sym p) β q _β‘β¨β©_ : β {β} {A : Type β} (x : A) {y : A} β x β‘ y β x β‘ y x β‘β¨β© xβ‘y = xβ‘y _β : β {β} {A : Type β} (x : A) β x β‘ x x β = refl infixr 30 _β_ infixr 2 _β‘β¨β©_ _β‘Λβ¨_β©_ infix 3 _β

These functions are used to make *equational reasoning chains*. For instance, the following proof that addition of naturals is associative is done in equational reasoning style:

private +-associative : (x y z : Nat) β (x + y) + z β‘ x + (y + z) +-associative zero y z = refl +-associative (suc x) y z = suc ((x + y) + z) β‘β¨ ap suc (+-associative x y z) β©β‘ suc (x + (y + z)) β

If your browser runs JavaScript, these equational reasoning chains, by default, render with the *justifications* (the argument written between `β¨ β©`

) hidden; There is a checkbox to display them, either on the sidebar or on the top bar depending on how narrow your screen is. For your convenience, itβs here too:

Try pressing it!

# Dependent Pathsπ

Surprisingly often, we want to compare inhabitants $a : A$ and $b : B$ where the types $A$ and $B$ are not *definitionally* equal, but only identified in some specified way. We call these β**paths** over **p**paths,β or PathP for short. In the same way that a Path can be understood as a function `I β A`

with specified endpoints, a PathP (*path* over *p*ath) can be understood as a *dependent* function `(i : I) β A i`

.

In the Book, paths over paths are implemented in terms of the transport operation: A path `x β‘ y`

over `p`

is a path `transport p x β‘ y`

, thus defining dependent identifications using non-dependent ones. Fortunately, a cubical argument shows us that these notions coincide:

PathPβ‘Path : β {β} (P : I β Type β) (p : P i0) (q : P i1) β PathP P p q β‘ Path (P i1) (transport (Ξ» i β P i) p) q PathPβ‘Path P p q i = PathP (Ξ» j β P (i β¨ j)) (transport-filler (Ξ» j β P j) p i) q PathPβ‘Pathβ» : β {β} (P : I β Type β) (p : P i0) (q : P i1) β PathP P p q β‘ Path (P i0) p (transport (Ξ» i β P (~ i)) q) PathPβ‘Pathβ» P p q i = PathP (Ξ» j β P (~ i β§ j)) p (transport-filler (Ξ» j β P (~ j)) q i)

We can see this by substituting either `i0`

or `i1`

for the variable `i`

.

When

`i = i0`

, we have`PathP (Ξ» j β P j) p q`

, by the endpoint rule for transport-filler.When

`i = i1`

, we have`PathP (Ξ» j β P i1) (transport P p) q`

, again by the endpoint rule for transport-filler.

The existence of paths over paths gives another βcounterexampleβ to thinking of paths as *equality*. For instance, itβs hard to imagine a world in which `true`

and `false`

can be equal in any interesting sense of the word *equal* β but over the identification $\id{Bool} \equiv \id{Bool}$ that switches the points around, `true`

and `false`

can be identified!

## Coercionπ

In Cubical Agda, the interval is given the structure of a De Morgan algebra. This is not the only choice of structure on the interval that gives a model of univalent type theory: We could also subject the interval to *no* additional structure other than what comes from the structural rules of type theory (introducing variables, ignoring variables, swapping variables, etc). This is a different cubical type theory, called *Cartesian cubical type theory*.

In Cartesian cubical type theory, instead of having a transp operation which takes $A(\id{i0}) \to A(\id{i1})$, there is a βmore powerfulβ *coercion* operation, written $\id{coe}^A_{i \to j}$, which takes $A(i) \to A(j)$, as in the subscript. However, despite the seeming added power, the coercion operation can be implemented in Cubical Agda: First, we introduce alternative names for several uses of transp.

coe0β1 : β {β} (A : I β Type β) β A i0 β A i1 coe0β1 A a = transp (Ξ» i β A i) i0 a -- ^ This is another name for transport coe1β0 : β {β} (A : I β Type β) β A i1 β A i0 coe1β0 A a = transp (Ξ» i β A (~ i)) i0 a -- ^ This is equivalent to transport β sym

There are also βmore excitingβ operations, which transport from one of the endpoints to a path which can vary over the interval. These generalise the transport-filler operation.

coe0βi : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i0 β A i coe0βi A i a = transp (Ξ» j β A (i β§ j)) (~ i) a coe1βi : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i1 β A i coe1βi A i a = transp (Ξ» j β A (i β¨ ~ j)) i a

We visualise coe0βi and coe1βi as being βspreadβ operations, since they take a value from one endpoint of the interval (0 or 1, respectively) and βspread itβ to a line varying over the variable `i`

. Similarly, we have βsqueezeβ operations, which take a line varying over `i`

to one of the endpoints:

coeiβ0 : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i β A i0 coeiβ0 A i a = transp (Ξ» j β A (i β§ ~ j)) (~ i) a

Using the filler of a square, we can put together the `0βi`

and `1βi`

coercions to get the βmaster coercionβ operation. That square is drawn as the diagram below, where the edges are more important than the corners, and the dashed line is `coe A i i1`

.

coe : β {β : I β Level} (A : β i β Type (β i)) (i j : I) β A i β A j coe A i j a = fill A (Ξ» j β Ξ» { (i = i0) β coe0βi A j a ; (i = i1) β coe1βi A j a }) (inS (coeiβ0 A i a)) j

As the square implies, when `j = i1`

, we have the squeeze operation opposite to coeiβ0, which we call coeiβ1.

coeiβ1 : β {β : I β Level} (A : β i β Type (β i)) (i : I) β A i β A i1 coeiβ1 A i a = coe A i i1 a

**Sidenote**: The boundary for the square implies that we can give a more verbose type for coe, one which mentions all of the spreads and squeezes. Note that this is a *dependent path between functions $A\ i \to A\ j$*, a very complicated construction indeed!

private coe-verbose : β {β} (A : I β Type β) β PathP (Ξ» i β PathP (Ξ» j β A i β A j) (coeiβ0 A i) (coeiβ1 A i)) (Ξ» j β coe0βi A j) (Ξ» j β coe1βi A j) coe-verbose A i j = coe A i j

This operation satisfies, *definitionally*, a whole host of equations. For starters, we have that the $\id{coe}^A_{i\to1}$ (resp $i \to 0$) specialises to transport when $i = 0$ (resp. $i = 1$), and to the identity when $i = 1$ (resp. $i = 0$):

coei0β1 : β {β} (A : I β Type β) (a : A i0) β coeiβ1 A i0 a β‘ coe0β1 A a coei0β1 A a = refl coei1β1 : β {β} (A : I β Type β) (a : A i1) β coeiβ1 A i1 a β‘ a coei1β1 A a = refl coei1β0 : β {β} (A : I β Type β) (a : A i1) β coeiβ0 A i1 a β‘ coe1β0 A a coei1β0 A a = refl coei0β0 : β {β} (A : I β Type β) (a : A i0) β coeiβ0 A i0 a β‘ a coei0β0 A a = refl

Then we have paths connecting the βmaster coercionβ coe and its several faces:

coeiβi0 : β {β} (A : I β Type β) (i : I) (a : A i) β coe A i i0 a β‘ coeiβ0 A i a coeiβi0 A i a = refl coei0βi : β {β} (A : I β Type β) (i : I) (a : A i0) β coe A i0 i a β‘ coe0βi A i a coei0βi A i a = refl coeiβi1 : β {β} (A : I β Type β) (i : I) (a : A i) β coe A i i1 a β‘ coeiβ1 A i a coeiβi1 A i a = refl coei1βi : β {β} (A : I β Type β) (i : I) (a : A i1) β coe A i1 i a β‘ coe1βi A i a coei1βi A i a = refl

In Cartesian cubical type theory, the following equation is definitional. It says that the top right and bottom left corners of the diagram are indeed what I said they were! However, in Cubical Agda, it is only propositional:

coeiβi : β {β} (A : I β Type β) (i : I) (a : A i) β coe A i i a β‘ a coeiβi A i = coe0βi (Ξ» i β (a : A i) β coe A i i a β‘ a) i (Ξ» _ β refl)

Using the Cartesian coercions, we define maps that convert between PathPs and Book dependent paths. These maps could also be defined in terms of transp and PathPβ‘Path, but this definition is more efficient.

to-pathp : β {β} {A : I β Type β} {x : A i0} {y : A i1} β coe0β1 A x β‘ y β PathP A x y to-pathp {A = A} {x} p i = hcomp (Ξ» j β Ξ» { (i = i0) β x ; (i = i1) β p j }) (coe0βi A i x) from-pathp : β {β} {A : I β Type β} {x : A i0} {y : A i1} β PathP A x y β coe0β1 A x β‘ y from-pathp {A = A} p i = coeiβ1 A i (p i)

These definitions illustrate how using the named squeezes and spreads β coe0βi, coeiβ1 β can be a lot more elegant than trying to work out what composition to use in a transp.

# Path Spacesπ

A large part of the study of HoTT is the *characterisation of path spaces*. Given a type `A`

, what does `Path A x y`

look like? Hedbergβs theorem says that for types with decidable equality, itβs boring. For the circle, we can prove its loop space is the integers β we have `Path SΒΉ base base β‘ Int`

.

Most of these characterisations need machinery that is not in this module to be properly stated. Even then, we can begin to outline a few simple cases:

## Ξ£ Typesπ

For Ξ£ types, a path between `(a , b) β‘ (x , y)`

consists of a path `p : a β‘ x`

, and a path between `b`

and `y`

laying over `p`

.

Ξ£-pathp : β {a b} {A : Type a} {B : A β Type b} β {x y : Ξ£ B} β (p : x .fst β‘ y .fst) β PathP (Ξ» i β B (p i)) (x .snd) (y .snd) β x β‘ y Ξ£-pathp p q i = p i , q i

We can also use the book characterisation of dependent paths, which is simpler in the case where the Ξ£ represents a subset β i.e., `B`

is a family of propositions.

Ξ£-path : β {a b} {A : Type a} {B : A β Type b} β {x y : Ξ£ B} β (p : x .fst β‘ y .fst) β subst B p (x .snd) β‘ (y .snd) β x β‘ y Ξ£-path {A = A} {B} {x} {y} p q = Ξ£-pathp p (to-pathp q)

## Ξ typesπ

For dependent functions, the paths are *homotopies*, in the topological sense: `Path ((x : A) β B x) f g`

is the same thing as a function `I β (x : A) β B x`

β which we could turn into a product if we really wanted to.

happly : β {a b} {A : Type a} {B : A β Type b} {f g : (x : A) β B x} β f β‘ g β (x : A) β f x β‘ g x happly p x i = p i x

With this, we have made definitional yet another principle which is propositional in the HoTT book: *function extensionality*. Functions are identical precisely if they assign the same outputs to every input.

funext : β {a b} {A : Type a} {B : A β Type b} {f g : (x : A) β B x} β ((x : A) β f x β‘ g x) β f β‘ g funext p i x = p x i

Furthermore, we know (since types are groupoids, and functions are functors) that, by analogy with 1-category theory, paths in a function type should behave like natural transformations (because they are arrows in a functor category). This is indeed the case:

homotopy-natural : β {a b} {A : Type a} {B : Type b} β {f g : A β B} β (H : (x : A) β f x β‘ g x) β {x y : A} (p : x β‘ y) β H x β ap g p β‘ ap f p β H y homotopy-natural {f = f} {g = g} H p = J (Ξ» _ p β H _ β ap g p β‘ ap f p β H _) (sym (β-filler (H _) refl) β β-filler' refl (H _)) p

## Pathsπ

The groupoid structure of *paths* is also interesting. While the characterisation of `Path (Path A x y) p q`

is fundamentally tied to the characterisation of `A`

, there are general theorems that can be proven about *transport* in path spaces. For example, substituting on both endpoints of a path is equivalent to a ternary composition:

subst-path-both : β {β} {A : Type β} {x y : A} β (loop : x β‘ x) β (adj : x β‘ y) β subst (Ξ» x β x β‘ x) adj loop β‘ sym adj β loop β adj subst-path-both loop adj = J (Ξ» _ adj β subst (Ξ» x β x β‘ x) adj loop β‘ sym adj β loop β adj) (sym lemma) adj where

The proof is by induction on the path `adj`

(for `adjustment`

): It suffices to consider the case where it is `refl`

. In that case, it becomes an application of the groupoid laws for types.

lemma : sym refl β loop β refl β‘ subst (Ξ» x β x β‘ x) refl loop lemma = sym refl β loop β refl β‘β¨β© refl β loop β refl β‘β¨ sym (β-filler' refl _) β©β‘ loop β refl β‘β¨ sym (β-filler _ refl) β©β‘ loop β‘β¨ sym (transport-refl _) β©β‘ subst (Ξ» x β x) refl loop β

Similar statements can be proven about substitution where we hold the right endpoint constant, in which case we get something homotopic to composing with the inverse of the adjustment:

subst-path-left : β {β} {A : Type β} {x y z : A} β (loop : x β‘ z) β (adj : x β‘ y) β subst (Ξ» e β e β‘ z) adj loop β‘ sym adj β loop subst-path-left {x = x} {y} {z} loop adj = J (Ξ» _ adj β subst (Ξ» e β e β‘ z) adj loop β‘ sym adj β loop) (sym lemma) adj where lemma : sym refl β loop β‘ subst (Ξ» e β e β‘ z) refl loop lemma = sym refl β loop β‘β¨β© refl β loop β‘β¨ sym (β-filler' refl _) β©β‘ loop β‘β¨ sym (transport-refl _) β©β‘ subst (Ξ» x β x) refl loop β

And for the case where we hold the left endpoint constant, in which case we get a respelling of composition:

subst-path-right : β {β} {A : Type β} {x y z : A} β (loop : x β‘ z) β (adj : z β‘ y) β subst (Ξ» e β x β‘ e) adj loop β‘ loop β adj subst-path-right {x = x} loop adj = J (Ξ» _ adj β subst (Ξ» e β x β‘ e) adj loop β‘ loop β adj) (sym lemma) adj where lemma : loop β refl β‘ subst (Ξ» e β x β‘ e) refl loop lemma = loop β refl β‘β¨ sym (β-filler _ refl) β©β‘ loop β‘β¨ sym (transport-refl _) β©β‘ subst (Ξ» x β x) refl loop β

The distinction between these two is elaborated on in the Intro to HoTT page.β©οΈ

For the semantically inclined, these correspond to face inclusions (including the inclusions of endpoints into a line) being monomorphisms, and thus

*cofibrations*in the model structure on cubical sets.β©οΈSince I is not Kan (that is β it does not have a

*composition*structure), it is not an inhabitant of the βfibrant universeβ Type. Instead it lives in`SSet`

, or, in Agda 2.6.3, its own universe β`IUniv`

.β©οΈI (AmΓ©lia) wrote a blog post explaining the semantics of them in a lot of depth.β©οΈ

Sub lives in the universe

`SSetΟ`

, which we do not have a binding for, so we can not name the type of _[_β¦_].β©οΈAlthough it is not proven to be a contradiction in

*this*module, see Data.Bool for that construction.β©οΈThis element has type

`(i : I) β I β Partial (~ i β¨ i) A`

rather than`(i : I) β Partial (~ i β¨ i) (I β A)`

because of a universe restriction in Agda: The second argument to Partial must be a Type, but I is not a Type.β©οΈIn Agda 2.6.2, function types

`I β A`

are*not*fibrant, even though they correspond to paths with βunmarkedβ endpoints. In Agda 2.6.3 (in development at the time of writing),`I`

was moved to its own universe,`IUniv`

, with a typing rule for functions saying that`A β B`

is fibrant whenever`B : Type`

and`A : Type`

*or*`A : IUniv`

- i.e. function types`I β A`

were made fibrant whenever`A`

is.β©οΈ