open import 1Lab.Type.Sigma
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

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 (2016) — 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
  A A₀ A₁ B B₀ B₁ C C₀ C₁ : Type ℓ

private 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 $φ = \neg i \lor 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 tys eqvs module glue-sys where
  tys : Partial φ (Type _)
  tys (φ = i1) = Te 1=1 .fst

  eqvs : PartialP φ (λ .o → tys _ ≃ A)
  eqvs (φ = i1) = Te 1=1 .snd

unattach
  : {A : Type ℓ} (φ : I) {T : Partial φ (Type ℓ')}
    {e : PartialP φ (λ o → T o ≃ A)}
  → primGlue A T e → A
unattach φ = prim^unglue {φ = φ}

attach
  : {A : Type ℓ} (φ : I) {T : Partial φ (Type ℓ')} {e : PartialP φ (λ o → T o ≃ A)}
  → (p : PartialP φ T)
  → A [ φ ↦ (λ o → e o .fst (p o)) ]
  → primGlue A T e
attach φ 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 $φ = i 1,$ 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 Types 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 $u 0$ 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 $u 0$ 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 \equiv B .$ Since Glue fills open boxes of types using equivalences, this path exists!

private module _ where private

  ua : {A B : Type ℓ} → A ≃ B → A ≡ B
  ua {A = A} {B} eqv i = Glue B λ where
    (i = i0) → A , eqv
    (i = i1) → B , _ , id-equiv

-- We use two named systems for the definition of 'ua' so that we can
-- make the Glue display away

ua : {A B : Type ℓ} → A ≃ B → A ≡ B
ua {A = A} {B} eqv i = primGlue B tys eqvs module ua-sys where
  tys : Partial (∂ i) (Type _)
  tys (i = i0) = A
  tys (i = i1) = B

  eqvs : PartialP (∂ i) (λ .o → tys o ≃ B)
  eqvs (i = i0) = eqv
  eqvs (i = i1) = id≃

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 \lor \neg 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 extension types, rather than using Paths, 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 = unattach (∂ i) x

-- Display of primGlue and ua
-- --------------------------
--
-- We can't in general recover a pretty Glue application from an
-- internal 'primGlue', since display forms can't do higher order
-- matching.
--
-- But we can instead use a *named* system in the definition
-- of important 'Glue's, and then match on this definition when trying
-- to unapply 'primGlue'.
--
-- Since 'primGlue' is private, the only way to glue things is using the
-- nice interface, so 'Glue's display nicely.

-- recover the primitives
{-# DISPLAY primGlue A (glue-sys.tys _ Te) (glue-sys.eqvs _ Te) = Glue A Te #-}
{-# DISPLAY prim^unglue {l} {l'} {A} {φ} {t} {e} x = unattach {l} {l'} {A} φ {t} {e} x #-}
{-# DISPLAY prim^glue {_} {_} {_} {φ} {_} {_} x y = attach φ x y #-}

-- recover ua specifically
{-# DISPLAY primGlue _ (ua-sys.tys e i) (ua-sys.eqvs _ _) = ua e i #-}
{-# DISPLAY unattach {_} {_} _ {ua-sys.tys {ℓ} {A} {B} f i} {ua-sys.eqvs _ _} x = ua-unglue {ℓ} {A} {B} f 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
ua-glue e i x y = 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 = 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-iso→is-equiv λ where
  .is-iso.from   → ua-pathp→path eqv
  .is-iso.linv x → refl
  .is-iso.rinv x → refl

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.from = 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 λ where
  .is-iso.from x → ua (x .lower)
  .is-iso.rinv x → ap lift (Path≃Equiv .snd .is-iso.rinv _)
  .is-iso.linv x → Path≃Equiv .snd .is-iso.linv _

Equivalence induction🔗

One useful consequence of $(A \equiv B) ≃ (A ≃ B)$ ¹ 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)
Equiv-is-contr A .centre            = A , _ , id-equiv
Equiv-is-contr A .paths (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 = 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 \to B$ is an equivalence. We want to show that, for any choice of $x, y : A,$ the map $ap (f) x, y : x \equiv y \to f (x) \equiv 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 \to Ω$ corresponds to maps $A \to 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 $(\infty, 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.

private variable
  E : Type ℓ
open is-iso

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) \to 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 .fst ((x , y) , p) = subst B p y
Fibre-equiv B a .snd = is-iso→is-equiv λ where
  .is-iso.from x   → (a , x) , refl
  .is-iso.rinv x i → coe1→i (λ _ → B a) i x
  .is-iso.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 \to 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 .fst x = p x , x , refl
Total-equiv p .snd = is-iso→is-equiv λ where
  .is-iso.from (_ , x , _)   → x
  .is-iso.rinv (b , x , q) i → q i , x , λ j → q (i ∧ j)
  .is-iso.linv x             → refl

Putting these together, we get the promised theorem: The space of maps $B \to Type$ is equivalent to the space of fibrations with base space $B$ and variable total space $E,$ $Σ_{(E : Type)} (E \to 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} .fst (E , p) = fibre p
Fibration-equiv {B = B} .snd = is-iso→is-equiv λ where
  .is-iso.from p⁻¹       → Σ _ p⁻¹ , fst
  .is-iso.rinv prep i x  → ua (Fibre-equiv prep x) i
  .is-iso.linv (E , p) i →
    let e = Total-equiv p
     in ua e (~ i) , λ x → ua-unglue e (~ i) x .fst

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.

_ = is-prop

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} (unattach φ)
unglue-is-equiv {A = A} φ {B = B} .is-eqv y = extend→is-contr ctr
  where module _ (ψ : I) (par : Partial ψ (fibre (unattach φ) 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 $ₛ attach φ (λ { (φ = 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-square
  : ∀ {ℓ} {W X Y Z : Type ℓ} {f : W ≃ X} {g : W ≃ Y} {g' : X ≃ Z} {f' : Y ≃ Z}
  → Path (W → Z) (λ x → g' .fst (f .fst x)) (λ x → f' .fst (g .fst x))
  → Square (ua f) (ua g) (ua g') (ua f')
ua-square {W = W} {X} {Y} {Z} {f} {g} {g'} {f'} p j k =
  Glue Z λ where
    (j = i0) → ua g  k , _ ,
      is-prop→pathp (λ j → is-equiv-is-prop {A = ua g  j} λ x → f' .fst (unattach (∂ j) x)) (∘-is-equiv (f' .snd) (g .snd)) (f' .snd) k
    (j = i1) → ua g' k , _ ,
      is-prop→pathp (λ i → is-equiv-is-prop {A = ua g' i} λ x → unattach (∂ i) x) (g' .snd) id-equiv k
    (k = i0) → ua f  j , _ ,
      is-prop→pathp (λ i → is-equiv-is-prop {A = ua f  i} λ x → p'' i x) (∘-is-equiv (f' .snd) (g .snd)) (g' .snd) j
    (k = i1) → ua f' j , _ ,
      is-prop→pathp (λ i → is-equiv-is-prop {A = ua f' i} λ x → unattach (∂ i) x) (f' .snd) id-equiv j
  where
    p'' : PathP (λ i → ua f i → Z) (λ z → f' .fst (g .fst z)) (g' .fst)
    p'' j x = hcomp (∂ j) λ where
      k (k = i0) → g' .fst (unattach (∂ j) x)
      k (j = i0) → p k x
      k (j = i1) → g' .fst x

ua-triangle
  : ∀ {ℓ} {A B C : Type ℓ} {e : A ≃ B} {f : A ≃ C} {g : B ≃ C}
  → Path (A → C) (f .fst) (λ x → g .fst (e .fst x))
  → Triangle (ua e) (ua f) (ua g)
ua-triangle α = transpose (sym ua-id-equiv ◁ transpose (ua-square α))

∙-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-inc : ∀ {ℓ} {A₀ A₁ : Type ℓ} (e : A₀ ≃ A₁) (x : A₀) (i : I) → ua e i
ua-inc e x i = ua-glue e i (λ ._ → x) (inS (e .fst x))

ua→
  : ∀ {e : A₀ ≃ A₁} {B : (i : I) → ua e i → Type ℓ'} {f₀ f₁}
  → (∀ a → PathP (λ i → B i (ua-inc e a i)) (f₀ a) (f₁ (e .fst a)))
  → PathP (λ i → (x : ua e i) → B i x) f₀ f₁
ua→ {e = e} {B} {f₀ = f₀} {f₁} h = (λ i a → comp (λ j → B (i ∨ ~ j) (x' i (~ j) a)) (∂ i) (sys i a)) module ua→ where
  x' : ∀ i j (x : ua e i) → ua e (i ∨ j)
  x' i j x = ua-glue e (i ∨ j) (λ { (i = i0) (j = i0) → x }) (inS (unattach (∂ i) x))

  sys : ∀ i (a : ua e i) j → Partial (∂ i ∨ ~ j) (B (i ∨ ~ j) (x' i (~ j) a))
  sys i a j (j = i0) = f₁ (unattach (∂ i) a)
  sys i a j (i = i0) = h a (~ j)
  sys i a j (i = i1) = f₁ a

  filler : ∀ i j (a : ua e i) → B (i ∨ ~ j) (x' i (~ j) a)
  filler i j a = fill (λ j → B (i ∨ ~ j) (x' i (~ j) a)) (∂ i) j (sys i a)

ua→'
  : ∀ {e : A₀ ≃ A₁} {B : (i : I) → ua e i → Type ℓ'} {f₀ : {a : A₀} → B i0 a} {f₁ : {a : A₁} → B i1 a}
  → (∀ a → PathP (λ i → B i (ua-inc e a i)) (f₀ {a}) (f₁ {e .fst a}))
  → PathP (λ i → {x : ua e i} → B i x) f₀ f₁
ua→' {B = B} {f₀} {f₁} h i {x} = ua→ {B = B} {f₀ = λ x → f₀ {x}} {f₁ = λ x → f₁ {x}} h 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)

transport-∙
  : ∀ {ℓ} {A B C : Type ℓ}
  → (p : A ≡ B) (q : B ≡ C) (u : A)
  → transport (p ∙ q) u ≡ transport q (transport p u)
transport-∙ = subst-∙ id

-- This is less dependent than it could be (in particular B could be A →
-- Type) but it is much simpler to use. (_∙P_ has terrible inference in
-- the B argument and we do not have fillers etc for it.)
subst₂-∙
  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} → (C : A → B → Type ℓ'')
  → {a b c : A} (p : a ≡ b) (q : b ≡ c)
  → {x y z : B} (α : x ≡ y) (β : y ≡ z)
  → (u : C a x)
  → subst₂ C (p ∙ q) (α ∙ β) u ≡ subst₂ C q β (subst₂ C p α u)
subst₂-∙ B p q α β Bx i =
  transport (ap₂ B (∙-filler' p q (~ i)) (∙-filler' α β (~ i)))
    (transport-filler-ext (ap₂ B p α) i Bx)

Not the fundamental theorem of engineering!↩︎

References

Cohen, Cyril, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2016. “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.” https://arxiv.org/abs/1611.02108.