module 1Lab.Univalence where

# Univalenceπ

In Homotopy Type Theory, **univalence** is the principle
stating that equivalent types can be
identified. When the book first came out,
there was no widely-accepted *computational* interpretation of
this principle, so it was added to the theory as an axiom: the
**univalence axiom**.

Precisely, the axiom as presented in the book consists of the following data (right under remark Β§2.10.4):

A map which turns equivalences into identifications of types. This map is called

`ua`

.A rule for eliminating identifications of types, by turning them into equivalences:

`pathβequiv`

The propositional computation rule, stating that transport along

`ua(f)`

is identical to applying`f`

:`uaΞ²`

.

In the book, there is an extra postulated datum asserting that `ua`

is an inverse to `pathβequiv`

. This datum does not
have a name in this development, because itβs proved in-line in the
construction of the term `univalence`

.

The point of cubical type theory is to give these terms constructive interpretations, i.e., make them definable in the theory, in terms of constructions that have computational behaviour. Letβs see how this is done.

## Glueπ

To even *state* univalence, we first have to make sure that
the concept of βpaths between typesβ makes sense in the first place. In
βBook HoTTβ, paths between types are a well-formed concept because the
path type is uniformly inductively defined for *everything* β
including universes. This is not the case in Cubical type theory, where
for paths in
$T$
to be well-behaved,
$T$
must be *fibrant*.

Since thereβs no obvious choice for how to interpret `hcomp`

in `Type`

, a fine solution is to
make `hcomp`

its own type former. This
is the approach taken by some Cubical type theories in the RedPRL school. Univalence in those type
theories is then achieved by adding a type former, called
`V`

, which turns an equivalence into a path.

In CCHM β and
therefore Cubical Agda β a different approach is taken, which combines
proving univalence with defining a fibrancy structure for the universe.
The core idea is to define a new type former, `Glue`

, which βgluesβ a partial type, along an
equivalence, to a total type.

private variable β β' : Level primitive primGlue : (A : Type β) {Ο : I} β (T : Partial Ο (Type β')) β (e : PartialP Ο (Ξ» o β T o β A)) β Type β' prim^glue : {A : Type β} {Ο : I} β {T : Partial Ο (Type β')} β {e : PartialP Ο (Ξ» o β T o β A)} β PartialP Ο T β A β primGlue A T e prim^unglue : {A : Type β} {Ο : I} β {T : Partial Ο (Type β')} β {e : PartialP Ο (Ξ» o β T o β A)} β primGlue A T e β A open import Prim.HCompU open import 1Lab.Equiv.FromPath

Glue : (A : Type β) β {Ο : I} β (Te : Partial Ο (Ξ£[ T β Type β' ] (T β A))) β Type β'

The public interface of `Glue`

demands a type
$A,$
called the *base type*, a formula
$Ο,$
and a partial type
$T$
which is equivalent to
$A.$
Since the equivalence is defined *inside* the partial element, it
can also (potentially) vary over the interval, so in reality we have a
*family* of partial types
$T$
and a *family* of partial equivalences
$TβA.$

In the specific case where we set
$Ο=Β¬iβ¨i,$
we can illustrate `Glue A (T, f)`

as the dashed line in the
square diagram below. The conceptual idea is that by βgluingβ
$T$
onto a totally defined type, we get a type which extends
$T.$

Glue A Te = primGlue A (Ξ» x β Te x .fst) (Ξ» x β Te x .snd) unglue : {A : Type β} (Ο : I) {T : Partial Ο (Type β')} {e : PartialP Ο (Ξ» o β T o β A)} β primGlue A T e β A unglue Ο = prim^unglue {Ο = Ο} glue-inc : {A : Type β} (Ο : I) β {Tf : Partial Ο (Ξ£[ B β Type β' ] B β A)} β (p : PartialP Ο (Ξ» { (Ο = i1) β Tf 1=1 .fst })) β A [ Ο β¦ (Ξ» { (Ο = i1) β Tf 1=1 .snd .fst (p 1=1) }) ] β Glue A Tf glue-inc Ο p x = prim^glue {Ο = Ο} p (outS x)

For `Glue`

to extend
$T,$
we add a computation rule which could be called a **boundary
condition**, since it specifies how `Glue`

behaves on the boundaries
of cubes. Concisely, when
$Ο=i1,$
we have that `Glue`

evaluates to the partial
type. This is exactly what it means for `Glue`

to extend
$T!$

module _ {A B : Type} {e : A β B} where private Glue-boundary : Glue B {i1} (Ξ» x β A , e) β‘ A Glue-boundary i = A

Furthermore, since we can turn any family of paths into a family of
equivalences, we can use the `Glue`

construct to implement
something with precisely the same interface as `hcomp`

for `Type`

:

glue-hfill : β {β} Ο (u : β i β Partial (Ο β¨ ~ i) (Type β)) β β i β Type β [ _ β¦ (Ξ» { (i = i0) β u i0 1=1 ; (Ο = i1) β u i 1=1 }) ]

The type of `glue-hfill`

is the same as that
of `hfill`

, but the type is stated
much more verbosely β so that we may define it without previous
reference to a `hcomp`

analogue. Like `hfill`

, `glue-hfill`

extends an open box
of types to a totally-defined cube. The type of `glue-hfill`

expresses this in
terms of extensions: We have a path (thatβs the `β i β`

binder) of `Type`

s which agrees with
`outS u0`

on the left endpoint, and with `u`

everywhere.

glue-hfill Ο u i = inS ( Glue (u i0 1=1) {Ο = Ο β¨ ~ i} Ξ» { (Ο = i1) β u i 1=1 , lineβequiv (Ξ» j β u (i β§ ~ j) 1=1) ; (i = i0) β u i0 1=1 , lineβequiv (Ξ» i β u i0 1=1) })

In the case for
$i=i0,$
we must glue
$u0$
onto itself using the identity equivalence. This guarantees that the
boundary of the stated type for `glue-hfill`

is satisfied.
However, since different faces of partial elements must agree where they
are defined, we can not use the identity equivalence directly, since
`lineβequiv refl`

is not definitionally the identity
equivalence.

When $Ο=Ο,$ hence where $u$ is defined, we glue the endpoint $u$ onto $u0$ using the equivalence generated by the path provided by $u$ itself! Itβs a family of partial paths, after all, and that can be turned into a family of partial equivalences.

Using `hcomp-unique`

and `glue-hfill`

together, we get a
internal characterisation of the fibrancy structure of the universe.
While `hcomp-unique`

may appear
surprising, it is essentially a generalisation of the uniqueness of path
compositions: Any open box has a contractible space of fillers.

hcompβ‘Glue : β {β} {Ο} (u : β i β Partial (Ο β¨ ~ i) (Type β)) β hcomp Ο u β‘ Glue (u i0 1=1) (Ξ» { (Ο = i1) β u i1 1=1 , lineβequiv (Ξ» j β u (~ j) 1=1) }) hcompβ‘Glue {Ο = Ο} u = hcomp-unique Ο u (glue-hfill Ο u)

## Paths from Glueπ

Since `Glue`

generalises `hcomp`

by allowing a partial
equivalence as its βtubeβ, rather than a partial path, it allows us to
turn any equivalence into a path, using a sort of βtrickβ: We consider
the *line* with endpoints
$A$
and
$B$
as an open cube to be filled. A filler for this line is exactly a path
$Aβ‘B.$
Since `Glue`

fills open boxes of types
using equivalences, this path exists!

ua : {A B : Type β} β A β B β A β‘ B ua {A = A} {B} eqv i = Glue B Ξ» { (i = i0) β A , eqv ; (i = i1) β B , _ , id-equiv }

Semantically, the explanation of `ua`

as completing a partial line
is sufficient. But we can also ask ourselves: Why does this definition
go through, *syntactically*? Because of the boundary condition
for Glue: when `i = i0`

, the whole thing evaluates to
`A`

, meaning that the left endpoint of the path is correct.
The same thing happens with the right endpoint.

The action of transporting along
`ua(f)`

can be described by chasing an element around the
diagram that illustrates Glue in the
$Ο=iβ¨Β¬i$
case, specialising to `ua`

. Keep in mind that, since
the right face of the diagram βpoints in the wrong directionβ, it must
be inverted. However, the inverse of the identity equivalence is the
identity equivalence, so nothing changes (for this example).

- The action that corresponds to the left face of the diagram is to
apply the underlying function of
`f`

. This contributes the`f .fst x`

part of the`uaΞ²`

term below.

- For the bottom face, we have a path rather than an equivalence, so
we must
`transport`

along it. In this case, the path is the reflexivity on`B`

, but in a more general`Glue`

construction, it might be a non-trivial path.

To compensate for this extra transport, we use `coe1βi`

, which connects
`f .fst x`

and
`transport (Ξ» i β B) (f .fst x)`

.

- Finally, we apply the inverse of the identity equivalence,
corresponding to the right face in the diagram. This immediately
computes away, and thus contributes nothing to the
`uaΞ²`

path.

uaΞ² : {A B : Type β} (f : A β B) (x : A) β transport (ua f) x β‘ f .fst x uaΞ² {A = A} {B} f x i = coe1βi (Ξ» _ β B) i (f .fst x)

Since `ua`

is a map that turns
equivalences into paths, we can compose it with a function that turns isomorphisms into equivalences to get the
map `IsoβPath`

.

IsoβPath : {A B : Type β} β Iso A B β A β‘ B IsoβPath (f , iiso) = ua (f , is-isoβis-equiv iiso)

## Paths over uaπ

The introduction and elimination forms for `Glue`

can be specialised to the
case of `ua`

, leading to the definitions
of `ua-glue`

and `ua-unglue`

below. Their types
are written in terms of interval variables and extensions, rather than using
`Path`

s, because these typings make
the structure of `Glue`

more explicit.

The first, `ua-unglue`

, tells us that if we
have some `x : ua e i`

(varying over an interval variable
`i`

), then we have an element of `B`

which agrees
with `e .fst x`

on the left and with `x`

on the
right.

ua-unglue : β {A B : Type β} (e : A β B) (i : I) (x : ua e i) β B ua-unglue e i x = unglue (i β¨ ~ i) x

We can factor the interval variable out, to get a type in terms of
`PathP`

, leading to an
explanation of `ua-unglue`

without mentioning extensions: A
path `x β‘ y`

over `ua e`

induces a path
`e .fst x β‘ y`

.

ua-pathpβpath : β {A B : Type β} (e : A β B) {x : A} {y : B} β PathP (Ξ» i β ua e i) x y β e .fst x β‘ y ua-pathpβpath e p i = ua-unglue e i (p i)

In the other direction, we have `ua-glue`

, which expresses that a
path `e .fst x β‘ y`

implies that `x β‘ y`

over
`ua e`

. For the type of `ua-glue`

, suppose that we have a
partial element
$x$
defined on the left endpoint of the interval, together with an extension
$y$
of
$e(x)$
where
$x$
is defined. What `ua-glue`

expresses is that we
can complete this to a path in
$ua(e),$
which agrees with
$x$
and
$y$
where these are defined.

ua-glue : β {A B : Type β} (e : A β B) (i : I) (x : Partial (~ i) A) (y : B [ _ β¦ (Ξ» { (i = i0) β e .fst (x 1=1) }) ]) β ua e i [ _ β¦ (Ξ» { (i = i0) β x 1=1 ; (i = i1) β outS y }) ] ua-glue e i x y = inS (prim^glue {Ο = i β¨ ~ i} (Ξ» { (i = i0) β x 1=1 ; (i = i1) β outS y }) (outS y))

Observe that, since
$y$
is partially in the image of
$x,$
this essentially constrains
$x$
to be a βpartial preimageβ of
$y$
under the equivalence
$e.$
Factoring in the type of the interval, we get the promised map between
dependent paths over `ua`

and paths in B.

pathβua-pathp : β {A B : Type β} (e : A β B) {x : A} {y : B} β e .fst x β‘ y β PathP (Ξ» i β ua e i) x y pathβua-pathp e {x = x} p i = outS (ua-glue e i (Ξ» { (i = i0) β x }) (inS (p i)))

The βpathp to pathβ versions of the above lemmas are definitionally
inverses, so they provide a characterisation of
`PathP (ua f)`

in terms of non-dependent paths.

ua-pathpβpath : β {A B : Type β} (e : A β B) {x : A} {y : B} β (e .fst x β‘ y) β (PathP (Ξ» i β ua e i) x y) ua-pathpβpath eqv .fst = pathβua-pathp eqv ua-pathpβpath eqv .snd .is-eqv y .centre = strict-fibres (ua-pathpβpath eqv) y .fst ua-pathpβpath eqv .snd .is-eqv y .paths = strict-fibres (ua-pathpβpath eqv) y .snd

# The βaxiomβπ

The actual βunivalence axiomβ, as stated in the HoTT book, says that
the canonical map `A β‘ B`

, defined using `J`

, is an equivalence. This map
is `idβequiv`

, defined right above.
In more intuitive terms, itβs βcastingβ the identity equivalence
`A β A`

along a proof that `A β‘ B`

to get an
equivalence `A β B`

.

module _ where private idβequiv : {A B : Type β} β A β‘ B β A β B idβequiv {A = A} {B} = J (Ξ» x _ β A β x) (_ , id-equiv) idβequiv-refl : {A : Type β} β idβequiv (Ξ» i β A) β‘ (_ , id-equiv) idβequiv-refl {A = A} = J-refl (Ξ» x _ β A β x) (_ , id-equiv)

However, because of efficiency concerns (Agda *is* a
programming language, after all), instead of using `idβequiv`

defined using J, we
use `pathβequiv`

, which is defined in an auxiliary module.

pathβequiv : {A B : Type β} β A β‘ B β A β B pathβequiv p = lineβequiv (Ξ» i β p i)

Since identity of equivalences is determined by identity of their
underlying functions, to show that `pathβequiv`

of `refl`

is the identity
equivalence, we use `coe1βi`

to show that `transport`

by `refl`

is the identity.

pathβequiv-refl : {A : Type β} β pathβequiv (refl {x = A}) β‘ (id , id-equiv) pathβequiv-refl {A = A} = Ξ£-path (Ξ» i x β coe1βi (Ξ» i β A) i x) (is-propβpathp (Ξ» i β is-equiv-is-prop _) _ _)

For the other direction, we must show that `ua`

of `id-equiv`

is `refl`

. We can do this quite
efficiently using `Glue`

. Since this is a path
between paths, we have two interval variables.

ua-id-equiv : {A : Type β} β ua (_ , id-equiv {A = A}) β‘ refl ua-id-equiv {A = A} i j = Glue A {Ο = i β¨ ~ j β¨ j} (Ξ» _ β A , _ , id-equiv)

We can then prove that the map `pathβequiv`

is an isomorphism,
hence an equivalence. Itβs very useful to have explicit names for the
proofs that `pathβequiv`

and `ua`

are equivalences without
referring to components of `PathβEquiv`

, so we introduce
names for them as well.

PathβEquiv : {A B : Type β} β Iso (A β‘ B) (A β B) univalence : {A B : Type β} β is-equiv (pathβequiv {A = A} {B}) univalenceβ»ΒΉ : {A B : Type β} β is-equiv (ua {A = A} {B}) PathβEquiv {A = A} {B = B} = pathβequiv , iiso where iiso : is-iso pathβequiv iiso .is-iso.inv = ua

We show that `pathβequiv`

inverts `ua`

, which means proving that
one can recover the original equivalence from the generated path.
Because of the computational nature of Cubical Agda, all we have to do
is apply `uaΞ²`

:

iiso .is-iso.rinv (f , is-eqv) = Ξ£-path (funext (uaΞ² (f , is-eqv))) (is-equiv-is-prop f _ _)

For the other direction, we use path
induction to reduce the problem from showing that `ua`

inverts `pathβequiv`

for an arbitrary
path (which is hard) to showing that `pathβequiv`

takes `refl`

to the identity
equivalence (`pathβequiv-refl`

), and that
`ua`

takes the identity
equivalence to `refl`

(`ua-id-equiv`

).

iiso .is-iso.linv = J (Ξ» _ p β ua (pathβequiv p) β‘ p) (ap ua pathβequiv-refl β ua-id-equiv) univalence {A = A} {B} = is-isoβis-equiv (PathβEquiv .snd) univalenceβ»ΒΉ {A = A} {B} = is-isoβis-equiv (is-iso.inverse (PathβEquiv .snd))

In some situations, it is helpful to have a proof that `pathβequiv`

followed by `an adjustment of levels`

is still an equivalence:

univalence-lift : {A B : Type β} β is-equiv (Ξ» e β lift (pathβequiv {A = A} {B} e)) univalence-lift {β = β} = is-isoβis-equiv morp where morp : is-iso (Ξ» e β lift {β = lsuc β} (pathβequiv e)) morp .is-iso.inv x = ua (x .Lift.lower) morp .is-iso.rinv x = lift (pathβequiv (ua (x .Lift.lower))) β‘β¨ ap lift (PathβEquiv .snd .is-iso.rinv _) β©β‘ x β morp .is-iso.linv x = PathβEquiv .snd .is-iso.linv _

## Equivalence inductionπ

One useful consequence of
$(Aβ‘B)β(AβB)$^{1} is that the type of
*equivalences* satisfies the same
induction principle as the type of *identifications*. By
analogy with how path induction can be characterised as contractibility
of singletons and transport, βequivalence inductionβ can be
characterised as transport and contractibility of *singletons up to
equivalence*:

Equiv-is-contr : β {β} (A : Type β) β is-contr (Ξ£[ B β Type β ] A β B) is-contr.centre (Equiv-is-contr A) = A , _ , id-equiv is-contr.paths (Equiv-is-contr A) (B , AβB) i = ua AβB i , p i , q i where p : PathP (Ξ» i β A β ua AβB i) id (AβB .fst) p i x = outS (ua-glue AβB i (Ξ» { (i = i0) β x }) (inS (AβB .fst x))) q : PathP (Ξ» i β is-equiv (p i)) id-equiv (AβB .snd) q = is-propβpathp (Ξ» i β is-equiv-is-prop (p i)) _ _

Combining `Equiv-is-contr`

with `subst`

, we get an induction
principle for the type of equivalences based at
$A:$
To prove
$P(B,e)$
for any
$e:AβB,$
it suffices to consider the case where
$B$
is
$A$
and
$e$
is the identity equivalence.

EquivJ : β {β β'} {A : Type β} β (P : (B : Type β) β A β B β Type β') β P A (_ , id-equiv) β {B : Type β} (e : A β B) β P B e EquivJ P pid eqv = subst (Ξ» e β P (e .fst) (e .snd)) (Equiv-is-contr _ .is-contr.paths (_ , eqv)) pid

Equivalence induction simplifies the proofs of many properties about
equivalences. For example, if
$f$
is an equivalence, then so is its `action on paths`

$ap(f).$

private is-equivβis-embedding : β {β} {A B : Type β} β (f : A β B) β is-equiv f β {x y : A} β is-equiv (ap f {x = x} {y = y}) is-equivβis-embedding f eqv = EquivJ (Ξ» B e β is-equiv (ap (e .fst))) id-equiv (f , eqv)

The proof can be rendered in English roughly as follows:

Suppose $f:AβB$

`is an equivalence`

. We want to show that, for any choice of $x,y:A,$ the map $ap(f)_{x,y}:xβ‘yβf(x)β‘f(y)$ is an equivalence.By

`induction`

, it suffices to cover the case where $B$ is $A,$ and $f$ is the identity function.But then, we have that $ap(id)$ is definitionally equal to $id,$ which is known to be

`an equivalence`

. $β$

## Object classifiersπ

In category theory, the idea of *classifiers* (or
*classifying objects*) often comes up when categories applied to
the study of logic. For example, any elementary
topos has a *subobject
classifier*: an object
$Ξ©$
such that maps
$BβΞ©$
corresponds to maps
$AβB$
with propositional fibres (equivalently, inclusions
$AβͺB).$
In higher categorical analyses of logic, classifying objects exist for
more maps: an elementary **2**-topos has a discrete
object classifier, which classify maps with *discrete*
fibres.

Since a
$(1,1)-topos$
has classifiers for maps with
$(β1)-truncated$
fibres, and a
$(2,1)-topos$
has classifiers for maps with
$0-truncated$
fibres, one might expect that an $(β,1)-topos$
would have classifiers for maps with fibres that are not truncated at
all. This is indeed the case! In HoTT, this fact is internalised using
the univalent universes, and we can prove that univalent universes are
*object
classifiers*.

As an intermediate step, we prove that the value
$B(a)$
of a type family
$B$
at a point
$a$
is equivalent to the fibre of
$fst:Ξ£_{(x:A)}B(x)βA$
over
$a.$
The proof follows from the De Morgan structure on the interval, and the
βspreadβ operation `coe1βi`

.

-- HoTT book lemma 4.8.1 Fibre-equiv : (B : A β Type β') (a : A) β fibre (fst {B = B}) a β B a Fibre-equiv B a = IsoβEquiv isom where isom : Iso _ _ isom .fst ((x , y) , p) = subst B p y isom .snd .inv x = (a , x) , refl isom .snd .rinv x i = coe1βi (Ξ» _ β B a) i x isom .snd .linv ((x , y) , p) i = (p (~ i) , coe1βi (Ξ» j β B (p (~ i β§ ~ j))) i y) , Ξ» j β p (~ i β¨ j)

Another fact from homotopy theory that we can import into homotopy
*type* theory is that any map is equivalent to a fibration. More
specifically, given a map
$p:EβB,$
the total space
$E$
is equivalent to the dependent sum of the fibres. The theorems `Total-equiv`

and `Fibre-equiv`

are what justify
referring to `Ξ£`

the βtotal spaceβ of a type
family.

Total-equiv : (p : E β B) β E β Ξ£ B (fibre p) Total-equiv p = IsoβEquiv isom where isom : Iso _ (Ξ£ _ (fibre p)) isom .fst x = p x , x , refl isom .snd .inv (_ , x , _) = x isom .snd .rinv (b , x , q) i = q i , x , Ξ» j β q (i β§ j) isom .snd .linv x = refl

Putting these together, we get the promised theorem: The space of
maps
$BβType$
is equivalent to the space of fibrations with base space
$B$
and variable total space
$E,$
$Ξ£_{(E:Type)}(EβB).$
If we allow
$E$
and
$B$
to live in different universes, then the maps are classified by the
biggest universe in which they both fit, namely
`Type (β β β')`

. Note that the proof of `Fibration-equiv`

makes
fundamental use of `ua`

, to construct the witnesses
that taking fibres and taking total spaces are inverses. Without `ua`

, we could only get an
βisomorphism-up-to-equivalenceβ of types.

Fibration-equiv : β {β β'} {B : Type β} β (Ξ£[ E β Type (β β β') ] (E β B)) β (B β Type (β β β')) Fibration-equiv {B = B} = IsoβEquiv isom where isom : Iso (Ξ£[ E β Type _ ] (E β B)) (B β Type _) isom .fst (E , p) = fibre p isom .snd .inv pβ»ΒΉ = Ξ£ _ pβ»ΒΉ , fst isom .snd .rinv prep i x = ua (Fibre-equiv prep x) i isom .snd .linv (E , p) i = ua e (~ i) , Ξ» x β fst (ua-unglue e (~ i) x) where e = Total-equiv p

To solidify the explanation that object classifiers generalise the
$(nβ2)-truncated$
object classifiers you would find in a
$(n,1)-topos,$
we prove that any class of maps described by a property
$P$
which holds of all of its fibres (or even *structure* on all of
its fibres!) has a classifying object β the total space
$Ξ£P.$

For instance, if we take
$P$
to be the property of `being a proposition`

, this
theorem tells us that `Ξ£ is-prop`

classifies
*subobjects*. With the slight caveat that `Ξ£ is-prop`

is not closed under impredicative quantification, this corresponds
exactly to the notion of subobject classifier in a
$(1,1)-topos,$
since the maps with propositional fibres are precisely the injective
maps.

Since the type of βmaps into B with variable domain and P fibresβ has a very unwieldy description β both in words or in Agda syntax β we abbreviate it by $β/_{[P]}B.$ The notation is meant to evoke the idea of a slice category: The objects of $C/c$ are objects of the category $C$ equipped with choices of maps into $c.$ Similarly, the objects of $β/_{[P]}B$ are objects of the universe $TypeΒβ,$ with a choice of map $f$ into $B,$ such that $P$ holds for all the fibres of $f.$

_/[_]_ : β {β' β''} (β : Level) β (Type (β β β') β Type β'') β Type β' β Type _ _/[_]_ {β} β' P B = Ξ£ (Type (β β β')) Ξ» A β Ξ£ (A β B) Ξ» f β (x : B) β P (fibre f x)

The proof that the slice
$β/_{[P]}B$
is classified by
$Ξ£P$
follows from elementary properties of
$Ξ£$
types (namely: `reassociation`

, `distributivity`

of
$Ξ£$
over
$Ξ),$
and the classification theorem `Fibration-equiv`

. Really, the
most complicated part of this proof is rearranging the nested sum and
product types to a form to which we can apply `Fibration-equiv`

.

Map-classifier : β {β β' β''} {B : Type β'} (P : Type (β β β') β Type β'') β (β /[ P ] B) β (B β Ξ£ _ P) Map-classifier {β = β} {B = B} P = (Ξ£ _ Ξ» A β Ξ£ _ Ξ» f β (x : B) β P (fibre f x)) ββ¨ Ξ£-assoc β©β (Ξ£ _ Ξ» { (x , f) β (x : B) β P (fibre f x) }) ββ¨ Ξ£-ap-fst (Fibration-equiv {β' = β}) β©β (Ξ£ _ Ξ» A β (x : B) β P (A x)) ββ¨ Ξ£-Ξ -distrib eβ»ΒΉ β©β (B β Ξ£ _ P) ββ

module ua {β} {A B : Type β} = Equiv (ua {A = A} {B} , univalenceβ»ΒΉ) unglue-is-equiv : β {β β'} {A : Type β} (Ο : I) β {B : Partial Ο (Ξ£ (Type β') (_β A))} β is-equiv {A = Glue A B} (unglue Ο) unglue-is-equiv {A = A} Ο {B = B} .is-eqv y = extendβis-contr ctr where module _ (Ο : I) (par : Partial Ο (fibre (unglue Ο) y)) where fib : .(p : IsOne Ο) β fibre (B p .snd .fst) y [ (Ο β§ Ο) β¦ (Ξ» { (Ο = i1) (Ο = i1) β par 1=1 }) ] fib p = is-contrβextend (B p .snd .snd .is-eqv y) (Ο β§ Ο) _ sys : β j β Partial (Ο β¨ Ο β¨ ~ j) A sys j (j = i0) = y sys j (Ο = i1) = outS (fib 1=1) .snd (~ j) sys j (Ο = i1) = par 1=1 .snd (~ j) ctr = inS $β glue-inc Ο {Tf = B} (Ξ» { (Ο = i1) β outS (fib 1=1) .fst }) (inS (hcomp (Ο β¨ Ο) sys)) , (Ξ» i β hfill (Ο β¨ Ο) (~ i) sys) ua-unglue-is-equiv : β {β} {A B : Type β} (f : A β B) β PathP (Ξ» i β is-equiv (ua-unglue f i)) (f .snd) id-equiv ua-unglue-is-equiv f = is-propβpathp (Ξ» j β is-equiv-is-prop (ua-unglue f j)) (f .snd) id-equiv uaβ : β {β} {A B C : Type β} {f : A β B} {g : B β C} β ua (f βe g) β‘ ua f β ua g uaβ {β = β} {A} {B} {C} {f} {g} = β-unique (ua (f βe g)) Ξ» i j β Glue C Ξ» where (i = i0) β ua f j , (Ξ» x β g .fst (ua-unglue f j x)) , is-propβpathp (Ξ» j β is-equiv-is-prop (Ξ» x β g .fst (ua-unglue f j x))) ((f βe g) .snd) (g .snd) j (i = i1) β ua (f βe g) j , ua-unglue (f βe g) j , ua-unglue-is-equiv (f βe g) j (j = i0) β A , f βe g (j = i1) β ua g i , ua-unglue g i , ua-unglue-is-equiv g i sym-ua : β {β} {A B : Type β} (e : A β B) β sym (ua e) β‘ ua (e eβ»ΒΉ) sym-ua {A = A} {B = B} e i j = Glue B Ξ» where (i = i0) β ua e (~ j) , ua-unglue e (~ j) , ua-unglue-is-equiv e (~ j) (i = i1) β ua (e eβ»ΒΉ) j , (Ξ» x β e .fst (ua-unglue (e eβ»ΒΉ) j x)) , is-propβpathp (Ξ» j β is-equiv-is-prop Ξ» x β e .fst (ua-unglue (e eβ»ΒΉ) j x)) (((e eβ»ΒΉ) βe e) .snd) (e .snd) j (j = i0) β B , (Ξ» x β Equiv.Ξ΅ e x (~ i)) , is-propβpathp (Ξ» j β is-equiv-is-prop Ξ» x β Equiv.Ξ΅ e x (~ j)) id-equiv (((e eβ»ΒΉ) βe e) .snd) i (j = i1) β A , e uaβ : β {β β'} {Aβ Aβ : Type β} {e : Aβ β Aβ} {B : (i : I) β Type β'} {fβ : Aβ β B i0} {fβ : Aβ β B i1} β ((a : Aβ) β PathP B (fβ a) (fβ (e .fst a))) β PathP (Ξ» i β ua e i β B i) fβ fβ uaβ {B = B} {fβ = fβ} {fβ} h i a = comp (Ξ» j β B (i β¨ ~ j)) (β i) Ξ» where j (j = i0) β fβ (unglue (β i) a) j (i = i0) β h a (~ j) j (i = i1) β fβ a uaβ2 : β {β β' β''} {Aβ Aβ : Type β} {eβ : Aβ β Aβ} {Bβ Bβ : Type β'} {eβ : Bβ β Bβ} {C : (i : I) β Type β''} {fβ : Aβ β Bβ β C i0} {fβ : Aβ β Bβ β C i1} β (β a b β PathP C (fβ a b) (fβ (eβ .fst a) (eβ .fst b))) β PathP (Ξ» i β ua eβ i β ua eβ i β C i) fβ fβ uaβ2 h = uaβ (uaβ β h) transport-β : β {β} {A B C : Type β} β (p : A β‘ B) (q : B β‘ C) (u : A) β transport (p β q) u β‘ transport q (transport p u) transport-β p q x i = transport (β-filler' p q (~ i)) (transport-filler-ext p i x) subst-β : β {β β'} {A : Type β} β (B : A β Type β') β {x y z : A} (p : x β‘ y) (q : y β‘ z) (u : B x) β subst B (p β q) u β‘ subst B q (subst B p u) subst-β B p q Bx i = transport (ap B (β-filler' p q (~ i))) (transport-filler-ext (ap B p) i Bx)

Not the fundamental theorem of engineering!β©οΈ