module 1Lab.HLevel where

# h-Levelsπ

When working in type theory, the mathematical activities of
*proving* and *constructing* become intermingled, in a way
that sometimes poses serious complications: The *method* by which
a given statement
$P$
was proven may be relevant in the future, since it is, at heart, a
*construction* β of a term of type
$P.$
To tame this annoyance, an important pursuit in type theory is
identifying the statements
$P$
for which the construction *can not* matter. A simple example is
equality between natural numbers: there is no further construction that
could tell *proofs of
$4=4$*
apart.

In a homotopy type theory, where a general type might have
non-trivial identifications *all
the way up*, it becomes very useful to state that, at some point, a
given type stops having distinguishable *constructions*, and
instead has a unique *proof* β for which we could substitute any
*other* potential proof. We have already mentioned the example of
the natural numbers: there are a lot of different natural numbers, but
as soon as we have a pair
$x,y:N,$
if we have any
$p:xβ‘y,$
then itβs as good as *any other*
$q:xβ‘y.$

At this point, we should introduce the proper terminology, rather
than speaking of βprovingβ types and βconstructingβ types. We say that a
type
$T$
is a **proposition**, written `is-prop`

below, if any two of
its inhabitants are identified. Since every construction is invariant
under identifications (by definition), this means that any two putative
constructions
$x,y:T$
are indistinguishable β theyβre really the same
**proof**.

is-prop : β {β} β Type β β Type β is-prop T = (x y : T) β x β‘ y

The information that a type is a proposition can also be seen as a
form of *induction principle*: If
$A$
is a proposition, and
$P(x)$
is a type family over
$A,$
then constructing a section
$β_{b:A}P(b)$
can be done by showing
$P(a)$
for any
$a$
at all. If we had this induction principle, then we could recover the
notion of propositionality above by taking
$P(x)$
to be the family
$aβ‘x.$

subst-prop : β {β β'} {A : Type β} {P : A β Type β'} β is-prop A β β a β P a β β b β P b subst-prop {P = P} prop a pa b = subst P (prop a b) pa

Keep in mind that, *even if* a type
$T$
is a proposition, it might still be possible to project interesting data
*from* a proof
$t:T$
β but, were we to project this data from
$s:T$
instead, we would get something identical. Propositions abound: the
statement that
$T$
is a proposition turns out to be one, for example, as is the statement
that a function
$f:AβB$
is an equivalence.
Even though any two proofs that
$f$
is an equivalence are interchangeable, if weβre given such a proof, we
can project out the inverse
$BβA$
β and there might be a lot of functions
$BβA$
laying around!

Knowing about propositions, we can now rephrase our earlier statement
about the natural numbers: each identity type
$xβ‘_{N}y$
is a proposition. Types for which this statement holds are called
**sets**. A proof that a type
$T$
is a set is a licence to stop caring about *how* we show that
$x,y:T$
are identified β we even say that theyβre just
**equal**.

is-set : β {β} β Type β β Type β is-set A = (x y : A) β is-prop (x β‘ y)

While it may seem unusual to ever explicitly *ask* whether a
pair of proofs
$p,q:xβ‘_{T}y$
are identical, we might certainly end up in such a situation if weβre
comparing larger structures! For example, if
$G$
and
$H$
are groups, then it makes
perfect sense to ask whether homomorphisms
$f,g:GβH$
are identical. But the data of a group homomorphism consists of a
function
$f:GβH$
between the types underlying each group, *and* a value in the
type
$β_{x,y:G}f(xy)=f(x)f(y).$
Knowing that a group has an underlying set means that this type is a
proposition β this value is really a *proof* that
$f$
preserves multiplication, and we do not have to care about it.

Since a set is defined to be a type whose identity types are
propositions, itβs natural to ask: is there a name for a type
$T$
whose identity types are *sets*? The answer is yes! These are
called **groupoids**. We can extend this process
recursively to ask about any natural number of iterated identity types.
This is called the typeβs **h-level**. If weβre thinking of
a type
$T$
as a space, and of the identifications
$xβ‘_{T}y$
as paths, then the statement
β$T$
has h-level
$n$β
tells you that the homotopy groups
$Ο_{k}(T)$
for
$k>n$
are all zero.

Thinking about how much information
$T$
carries, we could say that a proposition carries the information of
whether it is true or false; a set carries the information of which
inhabitant weβre looking at; a groupoid carries that, and, additionally,
the set of symmetries of that inhabitant, and so on. From this
perspective, there are types which are even *less* interesting β
those that carry no information at all: the propositions *we
know* are inhabited. In traditional foundations, we might call this
a *singleton*; in homotopy type theory, we call them
**contractible**.

Making the notion concrete, to say that
$T$
is contractible means giving a point
$t:T,$
called the **centre of contraction**, and an operation
that, given a point
$s:T,$
yields a path
$tβ‘s.$
We will show below that every proposition is a set, which means that,
since the identity types of a proposition are all pointed, they are all
*contractible*. Thus, the contractible types naturally fit into
the hierarchy of h-levels.

record is-contr {β} (A : Type β) : Type β where constructor contr field centre : A paths : (x : A) β centre β‘ x open is-contr public

We can now write down the definition of `is-hlevel`

, as a function of the
type *and* the specific level. Note that, even though that being
a proposition is equivalent to having contractible identity types, weβll
define `is-hlevel`

so that it agrees
with our previous definition.

is-hlevel : β {β} β Type β β Nat β Type _ is-hlevel A 0 = is-contr A is-hlevel A 1 = is-prop A is-hlevel A (suc n) = (x y : A) β is-hlevel (Path A x y) n

The recursive definition above agrees with `is-set`

at level 2. We can also
take this opportunity to define the groupoids as the types for which
`is-hlevel`

holds at level 3.

_ : is-set A β‘ is-hlevel A 2 _ = refl is-groupoid : β {β} β Type β β Type β is-groupoid A = is-hlevel A 3

The traditional numbering for h-levels says that the *sets*
are at level zero, and that the propositions and contractible types are
at negative levels (-1 and -2, respectively). While there is no
*mathematical* benefit to using this numbering over starting at
zero, there are *social* benefits. For example, the groupoids (at
level 3) turn out to be the types underlying (univalent) 1-categories.

We will, therefore, sometimes use the historical numbering in prose.
To clarify the distinction, we will say that a type
$T$
is **of h-level
$n$**
if `is-hlevel T n`

holds and, when
using the traditional numbering, we will say that
$T$
is an
**$(nβ2)-type$**,
or is
**$(nβ2)-truncated$**.
For example, sets are *of h-level
$2,$*
but are
$0-types,$
or
$0-truncated.$

## Examplesπ

We can now mention some examples of types at the various h-levels, to
show that the notion is not vacuous. Starting at the contractible types,
the most obvious example is the *literal* singleton β or rather,
unit β type.

β€-is-contr : is-contr β€ β€-is-contr .centre = tt β€-is-contr .paths _ = refl

We have previously mentioned that path induction says that the
*singletons*, in the sense of *the subtype of
$A$
identical to a given
$a:A$*,
are also contractible. Even though we have a shorter cubical proof (used
in the *definition* of path induction), we can demonstrate the
application of path induction:

_ : (a : A) β is-contr (Ξ£[ b β A ] b β‘ a) _ = Ξ» t β record { centre = (t , refl) ; paths = Ξ» (s , p) β J' (Ξ» s t p β (t , refl) β‘ (s , p)) (Ξ» t β refl) p }

This provides an example of a type that is not literally
*defined* to be of a certain h-level, but there are also
geometric examples. One is the unit interval, defined as a higher
inductive type, which has *two* points and a path between
them.

data [0,1] : Type where ii0 : [0,1] ii1 : [0,1] seg : ii0 β‘ ii1

Thinking geometrically, the construction of the contraction βfixesβ the endpoint at zero, and βpulls inβ the other endpoint; in the process, the path between them becomes trivial. We also have a direct cubical proof that this results in a contractible type:

interval-contractible : is-contr [0,1] interval-contractible .centre = ii0 interval-contractible .paths ii0 i = ii0 interval-contractible .paths ii1 i = seg i interval-contractible .paths (seg i) j = seg (i β§ j)

## Propositions are setsπ

We have previously mentioned that *being a proposition* is a
proposition, when applied to a specific type. We will show this by
showing that every proposition is a set: since `is-prop`

is then a (dependent)
function valued in propositions, itβs also a proposition. Showing this
in axiomatic homotopy type theory is slightly tricky, but showing it in
cubical type theory is a remarkable application of lifting
properties.

First, weβll make the geometry of the problem clear: weβre given
points
$x,y:A$
and paths
$p,q:xβ‘y.$
What we want to show, that
$pβ‘q,$
is visualised as a *square*. In one dimension, say
$j,$
we have
$p(j)$
and
$q(j),$
and these are opposite faces in another dimension, say
$i.$

Recall that, by fibrancy of
$A,$
we can obtain such a square by displaying it as the missing
higher-dimensional face in some higher cube, then appealing to `hcomp`

. As the *base
face*, opposite to what we want in some new direction
$k,$
we choose the square that is constantly
$x.$
We then have to give terms filling the four boundary squares β these
will turn out to be very similar. Letβs focus on the
$i=i0$
square.

The diagram below illustrates the setup: in addition to $i$ varying horizontally and $j$ varying vertically, we now have $k$ varying βfront to backβ. At the $k=i0$ face, we have the constantly $x$ square; at $k=i1,$ the boundary is the dashed square weβre looking for. The $i=i0$ square is on the left, in red.

By abstracting over the
$k$
dimension, we can think of the boundary of the red square as giving a
path type β weβre looking to construct a path between
$x:A$
and
$p(j):A.$
But since
$A$
is a proposition, we *have* such a path! If we write
$Ξ±$
for the witness that `is-prop A`

, we find that we can fill
the
$i=i0$
square by
$Ξ±(x,p(j),k).$
All of the other squares follow this same reasoning. You can see them in
the code below.

is-propβis-set : is-prop A β is-set A is-propβis-set h x y p q i j = hcomp (β i β¨ β j) Ξ» where k (k = i0) β x k (j = i0) β h x x k k (j = i1) β h x y k k (i = i0) β h x (p j) k k (i = i1) β h x (q j) k

## For completeness, we can also diagram the solution above.

A minor snag, which is not relevant to the overall idea, is the
boundary *of the*
$Ξ±(x,p(j),k)$
square we used for
$i=i0.$
At
$j=i0,$
weβre left with
$Ξ±(x,x,k),$
and not just
$x.$
Practically, this means that the filler of the top face canβt be
$x,$
since that wouldnβt agree with the left face on their shared edge; It
has to be the odd-looking
$Ξ±(x,x,k)$
instead.

As an immediate application, we can show that defining the types of
h-level to be the propositions, rather than asking for
*contractible* identity types, does not make a difference in the
setup:

Path-is-hlevel' : (n : Nat) β is-hlevel A (suc n) β (x y : A) β is-hlevel (x β‘ y) n Path-is-hlevel' 0 ahl x y = record { centre = ahl x y ; paths = is-propβis-set ahl _ _ _ } Path-is-hlevel' (suc n) h x y = h x y

PathP-is-hlevel' : β {β} {A : I β Type β} (n : Nat) β is-hlevel (A i1) (suc n) β (x : A i0) (y : A i1) β is-hlevel (PathP A x y) n PathP-is-hlevel' {A = A} n ahl x y = subst (Ξ» e β is-hlevel e n) (sym (PathPβ‘Path A x y)) (Path-is-hlevel' n ahl _ _) Path-is-hlevelβis-hlevel : β {β} {A : Type β} n β (p : (x y : A) β is-hlevel (x β‘ y) n) β is-hlevel A (suc n) Path-is-hlevelβis-hlevel zero wit x y = wit x y .centre Path-is-hlevelβis-hlevel (suc n) wit = wit

### Upwards closureπ

The proof that propositions are sets extends by induction to a proof
that any
$n-type$
is an
$(n+1)-type.$
However, recall we started the hierarchy with the contractible types, so
that the propositions are not *literally* the base case. Weβre
still missing a proof that being contractible implies being a
proposition. Since we have some cubical momentum going, itβs not hard to
construct a homogeneous
composition that expresses that contractible types are
propositions:

is-contrβis-prop : is-contr A β is-prop A is-contrβis-prop C x y i = hcomp (β i) Ξ» where j (i = i0) β C .paths x j j (i = i1) β C .paths y j j (j = i0) β C .centre

Reading the code above as a diagram, we can see that this is
precisely the composition of `sym (C .paths x)`

with
`C .paths y`

. It would not have made any difference whether
we used the pre-existing definition of *path* composition, but
itβs always a good idea to practice writing `hcomp`

s.

With that base case, we can actually perform the inductive argument. A similar argument extends this to showing that any $n-type$ is a $(k+n)-type,$ for any offset $k.$

is-hlevel-suc : β {β} {A : Type β} (n : Nat) β is-hlevel A n β is-hlevel A (suc n) is-hlevel-suc 0 x = is-contrβis-prop x is-hlevel-suc 1 x = is-propβis-set x is-hlevel-suc (suc (suc n)) h x y = is-hlevel-suc (suc n) (h x y) is-hlevel-+ : β {β} {A : Type β} (n k : Nat) β is-hlevel A n β is-hlevel A (k + n) is-hlevel-+ n zero x = x is-hlevel-+ n (suc k) x = is-hlevel-suc _ (is-hlevel-+ n k x)

A very convenient specialisation of these arguments will allow us to lift a proof that $A$ is a proposition to a proof that it has any positive h-level.

is-propβis-hlevel-suc : β {β} {A : Type β} {n : Nat} β is-prop A β is-hlevel A (suc n) is-propβis-hlevel-suc {n = zero} aprop = aprop is-propβis-hlevel-suc {n = suc n} aprop = is-hlevel-suc (suc n) (is-propβis-hlevel-suc aprop)

is-contrβis-hlevel : β {β} {A : Type β} n β is-contr A β is-hlevel A n is-contrβis-hlevel zero c = c is-contrβis-hlevel (suc n) c = is-propβis-hlevel-suc (is-contrβis-prop c) is-setβis-hlevel+2 : β {β} {A : Type β} {n : Nat} β is-set A β is-hlevel A (2 + n) is-setβis-hlevel+2 aset x y = is-propβis-hlevel-suc (aset x y)

Finally, weβll bootstrap some results about the closure of $n-types$ under various operations. Here, we can immediately show that the identity types of an $n-type$ are again $n-types.$

Path-is-hlevel : (n : Nat) β is-hlevel A n β {x y : A} β is-hlevel (x β‘ y) n Path-is-hlevel zero ahl = record { centre = is-contrβis-prop ahl _ _ ; paths = is-propβis-set (is-contrβis-prop ahl) _ _ _ } Path-is-hlevel (suc n) ahl = is-hlevel-suc (suc n) ahl _ _ PathP-is-hlevel : β {A : I β Type β} (n : Nat) β is-hlevel (A i1) n β β {x y} β is-hlevel (PathP A x y) n PathP-is-hlevel {A = A} n ahl {x} {y} = subst (Ξ» e β is-hlevel e n) (sym (PathPβ‘Path A x y)) (Path-is-hlevel n ahl)

Note that, while a contractible type is not *literally*
defined to be a pointed proposition, these notions are equivalent.
Indeed, if a type is contractible *assuming* it is pointed, it is
a proposition, as the two arguments below show. This explains why
propositions are sometimes referred to as
*contractible-if-inhabited*, but we will not use this
terminology.

is-contr-if-inhabitedβis-prop : β {β} {A : Type β} β (A β is-contr A) β is-prop A is-contr-if-inhabitedβis-prop cont x y = is-contrβis-prop (cont x) x y is-propββis-contr : β {β} {A : Type β} β is-prop A β A β is-contr A is-propββis-contr prop x .centre = x is-propββis-contr prop x .paths y = prop x y

### Propositionality of truncatednessπ

With upwards closure out of the way, we can show that being a proposition is a proposition. We have already mentioned it, and gestured towards the proof: since every proposition is a set, any two functions $Ξ±,Ξ²:β_{x,y:A}xβ‘y$ must agree, pointwise, on any $x,y:A.$ The code is similarly simple:

is-prop-is-prop : is-prop (is-prop A) is-prop-is-prop Ξ± Ξ² i x y = is-propβis-set Ξ± x y (Ξ± x y) (Ξ² x y) i

To show that being contractible is a proposition, weβll use a similar argument. It will suffice to show that the centres of contraction are identical, and that, over this, we have an identification between the contractions. This has a delightfully short proof also:

is-contr-is-prop : is-prop (is-contr A) is-contr-is-prop cβ cβ i .centre = cβ .paths (cβ .centre) i is-contr-is-prop cβ cβ i .paths x j = hcomp (β i β¨ β j) Ξ» where k (i = i0) β cβ .paths (cβ .paths x j) k k (i = i1) β cβ .paths (cβ .paths x j) k k (j = i0) β cβ .paths (cβ .paths (cβ .centre) i) k k (j = i1) β cβ .paths x k k (k = i0) β cβ .centre

Once again, we can extend this pair of base cases to the entire hierarchy, by an inductive argument of the same shape as the one we used for upwards closure.

is-hlevel-is-prop : β {β} {A : Type β} (n : Nat) β is-prop (is-hlevel A n) is-hlevel-is-prop 0 = is-contr-is-prop is-hlevel-is-prop 1 = is-prop-is-prop is-hlevel-is-prop (suc (suc n)) x y i a b = is-hlevel-is-prop (suc n) (x a b) (y a b) i

is-hlevel-is-hlevel-suc : β {β} {A : Type β} (k n : Nat) β is-hlevel (is-hlevel A n) (suc k) is-hlevel-is-hlevel-suc k n = is-propβis-hlevel-suc (is-hlevel-is-prop n)

## Dependent h-levelsπ

When working in a homotopy type theory, we often have to consider, in
addition to identity types, *dependent* identity types; in
cubical type theory, these are the primitive notion, implemented by
`PathP`

s. Regardless, it makes
sense to extend the notion of h-level to talk not only about
identifications in a type, but about arbitrary *dependent*
identifications in a *family* of types.

Rather than novelty, this notion of **dependent
h-level** does turn out to have practical applications β except
for the dependent analogue to *contractibility*. Therefore, we
bootstrap this notion with the *dependent propositions*: A family
$P(x)$
over
$X$
is a dependent proposition if any pair of elements are identified, over
an arbitrary path in the base:

is-hlevel-dep : β {β β'} {A : Type β} β (A β Type β') β Nat β Type _ is-hlevel-dep B zero = β {x y} (Ξ± : B x) (Ξ² : B y) (p : x β‘ y) β PathP (Ξ» i β B (p i)) Ξ± Ξ² is-hlevel-dep B (suc n) = β {a0 a1} (b0 : B a0) (b1 : B a1) β is-hlevel-dep {A = a0 β‘ a1} (Ξ» p β PathP (Ξ» i β B (p i)) b0 b1) n

However, there is an *emergent* notion of h-level for
families, namely, the pointwise lifting of the ordinary, non-dependent
h-levels. While the notion weβve just defined is more convenient to work
with cubically, weβre led to wonder how it compares to the pointwise
notion. Fortunately, they are equivalent.

is-propβpathp : β {B : I β Type β} β ((i : I) β is-prop (B i)) β β b0 b1 β PathP (Ξ» i β B i) b0 b1 is-propβpathp {B = B} hB b0 b1 = to-pathp (hB _ _ _)

The base case is usefully phrased as the helper lemma `is-propβpathp`

above: if we have
a *line of types*
$B(i)$
over
$i:I$
which is a proposition everywhere, then we can construct a `PathP`

over
$B$
between any points in the two fibres. The inductive case uses path
induction to focus on a single fibre:

is-hlevelβis-hlevel-dep : β {β β'} {A : Type β} {B : A β Type β'} β (n : Nat) β ((x : A) β is-hlevel (B x) (suc n)) β is-hlevel-dep B n is-hlevelβis-hlevel-dep zero hl Ξ± Ξ² p = is-propβpathp (Ξ» i β hl (p i)) Ξ± Ξ² is-hlevelβis-hlevel-dep {A = A} {B = B} (suc n) hl {a0} {a1} b0 b1 = is-hlevelβis-hlevel-dep n (Ξ» p β helper a1 p b1) where helper : (a1 : A) (p : a0 β‘ a1) (b1 : B a1) β is-hlevel (PathP (Ξ» i β B (p i)) b0 b1) (suc n) helper a1 p b1 = J (Ξ» a1 p β β b1 β is-hlevel (PathP (Ξ» i β B (p i)) b0 b1) (suc n)) (Ξ» _ β hl _ _ _) p b1

## Contractibility, geometricallyπ

In cubical type theory, rather than reasoning algebraically about
iterated identity types, we often prefer the more direct option of
reasoning in a higher-dimensional context, using lifting problems.
However, the notions of h-level we have defined all talk about these
iterated identity types. There is a more *natively cubical*
phrasing of contractiblity, which we now introduce, in terms of extensibility.

Suppose we have a partial element $Οβ’p:A$ defined on some cofibration $Ο.$ Does $p$ extend to a total element? If $A$ is contractible, yes! We have a base point $c:A,$ the centre of contraction, and, taking $Ο$ as the shape of a lifting problem, we can certainly find a system of partial paths $Οβ’cβ‘p$ β $A$ is a proposition, after all!

is-contrβextend : is-contr A β (Ο : I) (p : Partial Ο A) β A [ Ο β¦ p ] is-contrβextend C Ο p = inS do hcomp (Ο β¨ ~ Ο) Ξ» where j (j = i0) β C .centre j (Ο = i0) β C .centre j (Ο = i1) β C .paths (p 1=1) j

Conversely, if we know that every partial element
$A$
(with our choice of shape
$Ο)$
is extensible, we can prove that
$A$
is contractible. The centre is given by extending the *empty*
partial element, taking
$Ο=i0:$

extendβis-contr : (β Ο (p : Partial Ο A) β A [ Ο β¦ p ]) β is-contr A extendβis-contr ext .centre = outS (ext i0 Ξ» ())

To come up with a path connecting this empty extension and an $x:A,$ we can extend the partial element that is $x$ when $i=i1,$ and undefined everywhere. On the left endpoint, when $i=i0,$ this is exactly the empty system we used above!

extendβis-contr ext .paths x i = outS (ext i Ξ» _ β x)

We can use this to write a more direct proof that contractible types are sets, eliminating the passage through the proof that they are propositions.

is-contrβis-set : is-contr A β is-set A is-contrβis-set C x y p q i j = outS do is-contrβextend C (β i β¨ β j) Ξ» where (i = i0) β p j (i = i1) β q j (j = i0) β x (j = i1) β y

is-contrβpathp : β {B : I β Type β} β ((i : I) β is-contr (B i)) β (b0 : B i0) (b1 : B i1) β PathP (Ξ» i β B i) b0 b1 is-contrβpathp hB b0 b1 = is-propβpathp (Ξ» i β is-contrβis-prop (hB i)) b0 b1 SingletonP : β {β} (A : I β Type β) (a : A i0) β Type _ SingletonP A a = Ξ£[ x β A i1 ] PathP A a x SinglP-is-contr : β {β} (A : I β Type β) (a : A i0) β is-contr (SingletonP A a) SinglP-is-contr A a .centre = _ , transport-filler (Ξ» i β A i) a SinglP-is-contr A a .paths (x , p) i = _ , Ξ» j β fill A (β i) j Ξ» where j (i = i0) β coe0βi A j a j (i = i1) β p j j (j = i0) β a SinglP-is-prop : β {β} {A : I β Type β} {a : A i0} β is-prop (SingletonP A a) SinglP-is-prop = is-contrβis-prop (SinglP-is-contr _ _) is-propβsquarep : β {B : I β I β Type β} β ((i j : I) β is-prop (B i j)) β {a : B i0 i0} {b : B i0 i1} {c : B i1 i0} {d : B i1 i1} β (p : PathP (Ξ» j β B j i0) a c) β (q : PathP (Ξ» j β B i0 j) a b) β (s : PathP (Ξ» j β B i1 j) c d) β (r : PathP (Ξ» j β B j i1) b d) β SquareP B p q s r is-propβsquarep {B = B} is-propB {a = a} p q s r i j = hcomp (β j β¨ β i) Ξ» where k (j = i0) β is-propB i j (base i j) (p i) k k (j = i1) β is-propB i j (base i j) (r i) k k (i = i0) β is-propB i j (base i j) (q j) k k (i = i1) β is-propB i j (base i j) (s j) k k (k = i0) β base i j where base : (i j : I) β B i j base i j = transport (Ξ» k β B (i β§ k) (j β§ k)) a is-propβpathp-is-contr : {A : I β Type β} β ((i : I) β is-prop (A i)) β (x : A i0) (y : A i1) β is-contr (PathP A x y) is-propβpathp-is-contr ap x y .centre = is-propβpathp ap x y is-propβpathp-is-contr ap x y .paths p = is-propβsquarep (Ξ» i j β ap j) refl _ _ refl abstract is-setβsquarep : {A : I β I β Type β} (is-set : (i j : I) β is-set (A i j)) β {a : A i0 i0} {b : A i0 i1} {c : A i1 i0} {d : A i1 i1} β (p : PathP (Ξ» j β A j i0) a c) β (q : PathP (Ξ» j β A i0 j) a b) β (s : PathP (Ξ» j β A i1 j) c d) β (r : PathP (Ξ» j β A j i1) b d) β SquareP A p q s r is-setβsquarep isset aββ aββ aββ aββ = transport (sym (PathPβ‘Path _ _ _)) (PathP-is-hlevel' 1 (isset _ _) _ _ _ _) -- Has to go through: _ : β {A : Type} {a b c d : A} (p : a β‘ c) (q : a β‘ b) (s : c β‘ d) (r : b β‘ d) β Square p q s r β‘ SquareP (Ξ» _ _ β A) p q s r _ = Ξ» _ _ _ _ β refl is-setβcast-pathp : β {β β'} {A : Type β} {x y : A} {p q : x β‘ y} (P : A β Type β') {px : P x} {py : P y} β is-set A β PathP (Ξ» i β P (p i)) px py β PathP (Ξ» i β P (q i)) px py is-setβcast-pathp {p = p} {q = q} P {px} {py} set r = coe0β1 (Ξ» i β PathP (Ξ» j β P (set _ _ p q i j)) px py) r is-setβsubst-refl : β {β β'} {A : Type β} {x : A} β (P : A β Type β') β is-set A β (p : x β‘ x) β (px : P x) β subst P p px β‘ px is-setβsubst-refl {x = x} P set p px i = transp (Ξ» j β P (set x x p refl i j)) i px