module 1Lab.Equiv where

EquivalencesšŸ”—

The big idea of homotopy type theory is that isomorphic types can be identified: the univalence axiom. However, the notion of isomorphism, is, in a sense, not ā€œcoherentā€ enough to be used in the definition. For that, we need a coherent definition of equivalence, where ā€œbeing an equivalenceā€ is a proposition.

To be more specific, what we need for a notion of equivalence is-equivā”(f)\operatorname{is-equiv}(f) to be ā€œcoherentā€ is:

  • Being an isomorphism implies being an equivalence (is-isoā”(f)ā†’is-equivā”(f)\operatorname{is-iso}(f) \to \operatorname{is-equiv}(f))

  • Being an equivalence implies being an isomorphism (is-equivā”(f)ā†’is-isoā”(f)\operatorname{is-equiv}(f) \to \operatorname{is-iso}(f)); Taken together with the first point we may summarise: ā€œBeing an equivalence and being an isomorphism are logically equivalent.ā€

  • Most importantly, being an equivalence must be a proposition.

The notion we adopt is due to Voevodsky: An equivalence is one that has contractible fibres. Other definitions are possible (e.g.: bi-invertible maps) ā€” but contractible fibres are ā€œprivilegedā€ in Cubical Agda because for glueing to work, we need a proof that equivalences have contractible fibres anyway.

private
  variable
    ā„“ā‚ ā„“ā‚‚ : Level
    A B : Type ā„“ā‚

A homotopy fibre, fibre or preimage of a function f at a point y : B is the collection of all elements of A that f maps to y. Since many choices of name are possible, we settle on the one that is shortest and most aesthetic: fibre.

fibre : (A ā†’ B) ā†’ B ā†’ Type _
fibre f y = Ī£ _ Ī» x ā†’ f x ā‰” y

A function f is an equivalence if every one of its fibres is contractible - that is, for any element y in the range, there is exactly one element in the domain which f maps to y. Using set-theoretic language, f is an equivalence if the preimage of every element of the codomain is a singleton.

record is-equiv (f : A ā†’ B) : Type (level-of A āŠ” level-of B) where
  no-eta-equality
  field
    is-eqv : (y : B) ā†’ is-contr (fibre f y)

open is-equiv public

_ā‰ƒ_ : āˆ€ {ā„“ā‚ ā„“ā‚‚} ā†’ Type ā„“ā‚ ā†’ Type ā„“ā‚‚ ā†’ Type _
_ā‰ƒ_ A B = Ī£ (A ā†’ B) is-equiv

id-equiv : is-equiv {A = A} (Ī» x ā†’ x)
id-equiv .is-eqv y =
  contr (y , Ī» i ā†’ y)
    Ī» { (y' , p) i ā†’ p (~ i) , Ī» j ā†’ p (~ i āˆØ j) }

For Cubical Agda, the type of equivalences is distinguished, so we have to make a small wrapper to match the interface Agda expects. This is the geometric definition of contractibility, in terms of partial elements and extensibility.

{-# BUILTIN EQUIV _ā‰ƒ_ #-}
{-# BUILTIN EQUIVFUN fst #-}

is-eqv' : āˆ€ {a b} (A : Type a) (B : Type b)
        ā†’ (w : A ā‰ƒ B) (a : B)
        ā†’ (Ļˆ : I)
        ā†’ (p : Partial Ļˆ (fibre (w .fst) a))
        ā†’ fibre (w .fst) a [ Ļˆ ā†¦ p ]
is-eqv' A B (f , is-equiv) a Ļˆ u0 = inS (
  hcomp (āˆ‚ Ļˆ) Ī» where
    i (Ļˆ = i0) ā†’ c .centre
    i (Ļˆ = i1) ā†’ c .paths (u0 1=1) i
    i (i = i0) ā†’ c .centre)
  where c = is-equiv .is-eqv a

{-# BUILTIN EQUIVPROOF is-eqv' #-}

is-equiv is propositionalšŸ”—

A function can be an equivalence in at most one way. This follows from propositions being closed under dependent products, and is-contr being a proposition.

module _ where private
  is-equiv-is-prop : (f : A ā†’ B) ā†’ is-prop (is-equiv f)
  is-equiv-is-prop f x y i .is-eqv p = is-contr-is-prop (x .is-eqv p) (y .is-eqv p) i
Even though the proof above works, we use the direct cubical proof in this <details> tag (lifted from the Cubical Agda library) in the rest of the development for efficiency concerns.
is-equiv-is-prop : (f : A ā†’ B) ā†’ is-prop (is-equiv f)
is-equiv-is-prop f p q i .is-eqv y =
  let p2 = p .is-eqv y .paths
      q2 = q .is-eqv y .paths
  in contr (p2 (q .is-eqv y .centre) i) Ī» w j ā†’ hcomp (āˆ‚ i āˆØ āˆ‚ j) Ī» where
     k (i = i0) ā†’ p2 w j
     k (i = i1) ā†’ q2 w (j āˆØ ~ k)
     k (j = i0) ā†’ p2 (q2 w (~ k)) i
     k (j = i1) ā†’ w
     k (k = i0) ā†’ p2 w (i āˆØ j)

Isomorphisms from equivalencesšŸ”—

For this section, we need a definition of isomorphism. This is the same as ever! An isomorphism is a function that has a two-sided inverse. We first define what it means for a function to invert another on the left and on the right:

is-left-inverse : (B ā†’ A) ā†’ (A ā†’ B) ā†’ Type _
is-left-inverse g f = (x : _) ā†’ g (f x) ā‰” x

is-right-inverse : (B ā†’ A) ā†’ (A ā†’ B) ā†’ Type _
is-right-inverse g f = (x : _) ā†’ f (g x) ā‰” x

A proof that a function ff is an isomorphism consists of a function gg in the other direction, together with homotopies exhibiting gg as a left- and right- inverse to ff.

record is-iso (f : A ā†’ B) : Type (level-of A āŠ” level-of B) where
  no-eta-equality
  constructor iso
  field
    inv : B ā†’ A
    rinv : is-right-inverse inv f
    linv : is-left-inverse inv f

  inverse : is-iso inv
  inv inverse = f
  rinv inverse = linv
  linv inverse = rinv

Iso : āˆ€ {ā„“ā‚ ā„“ā‚‚} ā†’ Type ā„“ā‚ ā†’ Type ā„“ā‚‚ ā†’ Type _
Iso A B = Ī£ (A ā†’ B) is-iso

Any function that is an equivalence is an isomorphism:

equivā†’inverse : {f : A ā†’ B} ā†’ is-equiv f ā†’ B ā†’ A
equivā†’inverse eqv y = eqv .is-eqv y .centre .fst

equivā†’counit
  : āˆ€ {f : A ā†’ B} (eqv : is-equiv f) x ā†’ f (equivā†’inverse eqv x) ā‰” x
equivā†’counit eqv y = eqv .is-eqv y .centre .snd

equivā†’unit
  : āˆ€ {f : A ā†’ B} (eqv : is-equiv f) x ā†’ equivā†’inverse eqv (f x) ā‰” x
equivā†’unit {f = f} eqv x i = eqv .is-eqv (f x) .paths (x , refl) i .fst

equivā†’zig
  : āˆ€ {f : A ā†’ B} (eqv : is-equiv f) x
  ā†’ ap f (equivā†’unit eqv x) ā‰” equivā†’counit eqv (f x)
equivā†’zig {f = f} eqv x i j = hcomp (āˆ‚ i āˆØ āˆ‚ j) Ī» where
   k (i = i0) ā†’ f (equivā†’unit eqv x j)
   k (i = i1) ā†’ equivā†’counit eqv (f x) (j āˆØ ~ k)
   k (j = i0) ā†’ equivā†’counit eqv (f x) (i āˆ§ ~ k)
   k (j = i1) ā†’ f x
   k (k = i0) ā†’ eqv .is-eqv (f x) .paths (x , refl) j .snd i

equivā†’zag
  : āˆ€ {f : A ā†’ B} (eqv : is-equiv f) x
  ā†’ ap (equivā†’inverse eqv) (equivā†’counit eqv x)
  ā‰” equivā†’unit eqv (equivā†’inverse eqv x)
equivā†’zag {f = f} eqv b =
  subst (Ī» b ā†’ ap g (Īµ b) ā‰” Ī· (g b)) (Īµ b) (helper (g b)) where
  g = equivā†’inverse eqv
  Īµ = equivā†’counit eqv
  Ī· = equivā†’unit eqv

  helper : āˆ€ a ā†’ ap g (Īµ (f a)) ā‰” Ī· (g (f a))
  helper a i j = hcomp (āˆ‚ i āˆØ āˆ‚ j) Ī» where
    k (i = i0) ā†’ g (Īµ (f a) (j āˆØ ~ k))
    k (i = i1) ā†’ Ī· (Ī· a (~ k)) j
    k (j = i0) ā†’ g (equivā†’zig eqv a (~ i) (~ k))
    k (j = i1) ā†’ Ī· a (i āˆ§ ~ k)
    k (k = i0) ā†’ Ī· a (i āˆ§ j)

is-equivā†’is-iso : {f : A ā†’ B} ā†’ is-equiv f ā†’ is-iso f
is-iso.inv (is-equivā†’is-iso eqv) = equivā†’inverse eqv

We can get an element of x from the proof that f is an equivalence - itā€™s the point of A mapped to y, which we get from centre of contraction for the fibres of f over y.

is-iso.rinv (is-equivā†’is-iso eqv) y =
  eqv .is-eqv y .centre .snd

Similarly, that one fibre gives us a proof that the function above is a right inverse to f.

is-iso.linv (is-equivā†’is-iso {f = f} eqv) x i =
  eqv .is-eqv (f x) .paths (x , refl) i .fst

The proof that the function is a left inverse comes from the fibres of f over y being contractible. Since we have a fibre - namely, f maps x to f x by refl - we can get any other we want!

Equivalences from isomorphismsšŸ”—

Any isomorphism can be upgraded into an equivalence, in a way that preserves the function ff, its inverse gg, and the proof ss that gg is a right inverse to ff. We can not preserve everything, though, as is usual when making something ā€œmore coherentā€. Furthermore, if everything was preserved, is-iso would be a proposition, and this is provably not the case.

The argument presented here is done directly in cubical style, but a less direct proof is also available, by showing that every isomorphism is a half-adjoint equivalence, and that half-adjoint equivalences have contractible fibres.

module _ {f : A ā†’ B} (i : is-iso f) where

  open is-iso i renaming ( inv to g
                         ; rinv to s
                         ; linv to t
                         )

Suppose, then, that f:Aā†’Bf : A \to B and g:Bā†’Ag : B \to A, and weā€™re given witnesses s:f(gĀ x)=xs : f (g\ x) = x and t:g(fĀ x)=xt : g (f\ x) = x (named for section and retraction) that ff and gg are inverses. We want to show that, for any yy, the fibre of ff over yy is contractible. It suffices to show that the fibre is propositional, and that it is inhabited.

We begin with showing that the fibre over yy is propositional, since thatā€™s the harder of the two arguments. Suppose that we have yy, x0x_0, x1x_1, p0p_0 and p1p_1 as below; Note that (x0,p0)(x_0, p_0) and (x1,p1)(x_1, p_1) are fibres of ff over yy. What we need to show is that we have some Ļ€:x0ā‰”x1\pi : x_0 ā‰” x_1 and p0ā‰”p1p_0 ā‰” p_1 over Ļ€\pi.

  private module _ (y : B) (x0 x1 : A) (p0 : f x0 ā‰” y) (p1 : f x1 ā‰” y) where

As an intermediate step in proving that p0ā‰”p1p_0 ā‰” p_1, we must show that x0ā‰”x1x_0 ā‰” x_1 - without this, we canā€™t even state that p0p_0 and p1p_1 are identified, since they live in different types! To this end, we will build Ļ€:x0ā‰”x1\pi : x_0 ā‰” x_1, parts of which will be required to assemble the overall proof that p0ā‰”p1p_0 ā‰” p_1.

Weā€™ll detail the construction of Ļ€0\pi_0; for Ļ€1\pi_1, the same method is used. We want to construct a line, which we can do by exhibiting that line as the missing face in a square. We have equations gĀ yā‰”gĀ yg\ y ā‰” g\ y (refl), gĀ (fĀ x0)ā‰”gĀ yg\ (f\ x_0) ā‰” g\ y (the action of g on p0), and gĀ (fĀ x0)=x0g\ (f\ x_0) = x_0 by the assumption that gg is a right inverse to ff. Diagramatically, these fit together into a square:

The missing line in this square is Ļ€0\pi_0. Since the inside (the filler) will be useful to us later, we also give it a name: Īø\theta.

    Ļ€ā‚€ : g y ā‰” x0
    Ļ€ā‚€ i = hcomp (āˆ‚ i) Ī» where
      k (i = i0) ā†’ g y
      k (i = i1) ā†’ t x0 k
      k (k = i0) ā†’ g (p0 (~ i))

    Īøā‚€ : Square (ap g (sym p0)) refl (t x0) Ļ€ā‚€
    Īøā‚€ i j = hfill (āˆ‚ i) j Ī» where
      k (i = i0) ā†’ g y
      k (i = i1) ā†’ t x0 k
      k (k = i0) ā†’ g (p0 (~ i))

Since the construction of Ļ€1\pi_1 is analogous, Iā€™ll simply present the square. We correspondingly name the missing face Ļ€1\pi_1 and the filler Īø1\theta_1.

Joining these paths by their common gĀ yg\ y face, we obtain Ļ€:x0ā‰”x1\pi : x_0 ā‰” x_1. This square also has a filler, connecting Ļ€0\pi_0 and Ļ€1\pi_1 over the line gĀ yā‰”Ļ€Ā ig\ y ā‰” \pi\ i.

This concludes the construction of Ļ€\pi, and thus, the 2D part of the proof. Now, we want to show that p0ā‰”p1p_0 ā‰” p_1 over a path induced by Ļ€\pi. This is a square with a specific boundary, which can be built by constructing an appropriate open cube, where the missing face is that square. As an intermediate step, we define Īø\theta to be the filler for the square above.

    Īø : Square refl Ļ€ā‚€ Ļ€ā‚ Ļ€
    Īø i j = hfill (āˆ‚ i) j Ī» where
      k (i = i1) ā†’ Ļ€ā‚ k
      k (i = i0) ā†’ Ļ€ā‚€ k
      k (k = i0) ā†’ g y

Observe that we can coherently alter Īø\theta to get Ī¹\iota below, which expresses that apā”gĀ p0\operatorname{ap}g\ p_0 and apā”gĀ p1\operatorname{ap}g\ p_1 are identified.

    Ī¹ : Square (ap (g āˆ˜ f) Ļ€) (ap g p0) (ap g p1) refl
    Ī¹ i j = hcomp (āˆ‚ i āˆØ āˆ‚ j) Ī» where
      k (k = i0) ā†’ Īø i (~ j)
      k (i = i0) ā†’ Īøā‚€ (~ j) (~ k)
      k (i = i1) ā†’ Īøā‚ (~ j) (~ k)
      k (j = i0) ā†’ t (Ļ€ i) (~ k)
      k (j = i1) ā†’ g y

This composition can be visualised as the red (front) face in the diagram below. The back face is ĪøĀ iĀ (Ā¬Ā j)\theta\ i\ (\neg\ j), i.e.Ā (Īø i (~ j)) in the code. Similarly, the j=i1j = \mathrm{i1} (bottom) face is g y, the j=i0j = \mathrm{i0} (top) face is t (Ļ€ i) (~ k), and similarly for i=i0i = \mathrm{i0} (left) and i=i1i = \mathrm{i1} (right).

The fact that jj only appears as Ā¬j\neg j can be understood as the diagram above being upside-down. Indeed, Ļ€0\pi_0 and Ļ€1\pi_1 in the boundary of Īø\theta (the inner, blue face) are inverted when their types are considered. Weā€™re in the home stretch: Using our assumption s:f(gĀ x)=xs : f (g\ x) = x, we can cancel all of the fāˆ˜gf \circ gs in the diagram above to get what we wanted: p0ā‰”p1p_0 ā‰” p_1.

    sq1 : Square (ap f Ļ€) p0 p1 refl
    sq1 i j = hcomp (āˆ‚ i āˆØ āˆ‚ j) Ī» where
       k (i = i0) ā†’ s (p0 j) k
       k (i = i1) ā†’ s (p1 j) k
       k (j = i0) ā†’ s (f (Ļ€ i)) k
       k (j = i1) ā†’ s y k
       k (k = i0) ā†’ f (Ī¹ i j)

The composition above can be visualised as the front (red) face in the cubical diagram below. Once more, left is i=i0i = \mathrm{i0}, right is i=i1i = \mathrm{i1}, up is j=i0j = \mathrm{i0}, and down is j=i1j = \mathrm{i1}.

Putting all of this together, we get that (x0,p0)ā‰”(x1,p1)(x_0, p_0) ā‰” (x_1, p_1). Since there were no assumptions on any of the variables under consideration, this indeed says that the fibre over yy is a proposition for any choice of yy.

    is-isoā†’fibre-is-prop : (x0 , p0) ā‰” (x1 , p1)
    is-isoā†’fibre-is-prop i .fst = Ļ€ i
    is-isoā†’fibre-is-prop i .snd = sq1 i

Since the fibre over yy is inhabited by (gĀ y,sĀ y)(g\ y, s\ y), we get that any isomorphism has contractible fibres:

  is-isoā†’is-equiv : is-equiv f
  is-isoā†’is-equiv .is-eqv y .centre .fst = g y
  is-isoā†’is-equiv .is-eqv y .centre .snd = s y
  is-isoā†’is-equiv .is-eqv y .paths z =
    is-isoā†’fibre-is-prop y (g y) (fst z) (s y) (snd z)

Applying this to the Iso and _ā‰ƒ_ pairs, we can turn any isomorphism into a coherent equivalence.

Isoā†’Equiv : āˆ€ {ā„“ā‚ ā„“ā‚‚} {A : Type ā„“ā‚} {B : Type ā„“ā‚‚}
          ā†’ Iso A B
          ā†’ A ā‰ƒ B
Isoā†’Equiv (f , is-iso) = f , is-isoā†’is-equiv is-iso

A helpful lemma: Any function between contractible types is an equivalence:

is-contrā†’is-equiv : āˆ€ {ā„“ā‚ ā„“ā‚‚} {A : Type ā„“ā‚} {B : Type ā„“ā‚‚}
                  ā†’ is-contr A ā†’ is-contr B ā†’ {f : A ā†’ B}
                  ā†’ is-equiv f
is-contrā†’is-equiv cA cB = is-isoā†’is-equiv f-is-iso where
  f-is-iso : is-iso _
  is-iso.inv f-is-iso _ = cA .centre
  is-iso.rinv f-is-iso _ = is-contrā†’is-prop cB _ _
  is-iso.linv f-is-iso _ = is-contrā†’is-prop cA _ _

is-contrā†’ā‰ƒ : āˆ€ {ā„“ā‚ ā„“ā‚‚} {A : Type ā„“ā‚} {B : Type ā„“ā‚‚}
           ā†’ is-contr A ā†’ is-contr B ā†’ A ā‰ƒ B
is-contrā†’ā‰ƒ cA cB = (Ī» _ ā†’ cB .centre) , is-isoā†’is-equiv f-is-iso where
  f-is-iso : is-iso _
  is-iso.inv f-is-iso _ = cA .centre
  is-iso.rinv f-is-iso _ = is-contrā†’is-prop cB _ _
  is-iso.linv f-is-iso _ = is-contrā†’is-prop cA _ _

is-contrā†’ā‰ƒāŠ¤ : āˆ€ {ā„“} {A : Type ā„“} ā†’ is-contr A ā†’ A ā‰ƒ āŠ¤
is-contrā†’ā‰ƒāŠ¤ c = is-contrā†’ā‰ƒ c āŠ¤-is-contr

ā€¦and so is any function into an empty type:

Ā¬-is-equiv : āˆ€ {ā„“} {A : Type ā„“} (f : A ā†’ āŠ„) ā†’ is-equiv f
Ā¬-is-equiv f .is-eqv ()

is-emptyā†’ā‰ƒāŠ„ : āˆ€ {ā„“} {A : Type ā„“} ā†’ Ā¬ A ā†’ A ā‰ƒ āŠ„
is-emptyā†’ā‰ƒāŠ„ Ā¬a = _ , Ā¬-is-equiv Ā¬a

Equivalence ReasoningšŸ”—

To make composing equivalences more intuitive, we implement operators to do equivalence reasoning in the same style as equational reasoning.

_āˆ™e_ : āˆ€ {ā„“ ā„“ā‚ ā„“ā‚‚} {A : Type ā„“} {B : Type ā„“ā‚} {C : Type ā„“ā‚‚}
     ā†’ A ā‰ƒ B ā†’ B ā‰ƒ C ā†’ A ā‰ƒ C

_eā»Ā¹ : āˆ€ {ā„“ ā„“ā‚} {A : Type ā„“} {B : Type ā„“ā‚}
     ā†’ A ā‰ƒ B ā†’ B ā‰ƒ A
_eā»Ā¹ eqv = Isoā†’Equiv ( equivā†’inverse (eqv .snd)
                     , record { inv  = eqv .fst
                              ; rinv = equivā†’unit (eqv .snd)
                              ; linv = equivā†’counit (eqv .snd)
                              })
_āˆ™e_ (f , e) (g , e') = (Ī» x ā†’ g (f x)) , eqv where
  gā»Ā¹ : is-iso g
  gā»Ā¹ = is-equivā†’is-iso e'

  fā»Ā¹ : is-iso f
  fā»Ā¹ = is-equivā†’is-iso e

  inv : _ ā†’ _
  inv x = fā»Ā¹ .is-iso.inv (gā»Ā¹ .is-iso.inv x)

  abstract
    right : is-right-inverse inv (Ī» x ā†’ g (f x))
    right z =
      g (f (fā»Ā¹ .is-iso.inv (gā»Ā¹ .is-iso.inv z))) ā‰”āŸØ ap g (fā»Ā¹ .is-iso.rinv _) āŸ©ā‰”
      g (gā»Ā¹ .is-iso.inv z)                       ā‰”āŸØ gā»Ā¹ .is-iso.rinv _ āŸ©ā‰”
      z                                           āˆŽ

    left : is-left-inverse inv (Ī» x ā†’ g (f x))
    left z =
      fā»Ā¹ .is-iso.inv (gā»Ā¹ .is-iso.inv (g (f z))) ā‰”āŸØ ap (fā»Ā¹ .is-iso.inv) (gā»Ā¹ .is-iso.linv _) āŸ©ā‰”
      fā»Ā¹ .is-iso.inv (f z)                       ā‰”āŸØ fā»Ā¹ .is-iso.linv _ āŸ©ā‰”
      z                                           āˆŽ
  eqv : is-equiv (Ī» x ā†’ g (f x))
  eqv = is-isoā†’is-equiv (iso (Ī» x ā†’ fā»Ā¹ .is-iso.inv (gā»Ā¹ .is-iso.inv x)) right left)

infixr 30 _āˆ™e_
infix 31 _eā»Ā¹

āˆ™-is-equiv : āˆ€ {ā„“ ā„“ā‚ ā„“ā‚‚} {A : Type ā„“} {B : Type ā„“ā‚} {C : Type ā„“ā‚‚}
           ā†’ {f : A ā†’ B} {g : B ā†’ C}
           ā†’ is-equiv f
           ā†’ is-equiv g
           ā†’ is-equiv (Ī» x ā†’ g (f x))
āˆ™-is-equiv {f = f} {g = g} e e' = ((f , e) āˆ™e (g , e')) .snd

module Equiv {ā„“ ā„“ā€²} {A : Type ā„“} {B : Type ā„“ā€²} (f : A ā‰ƒ B) where
  to = f .fst
  from = equivā†’inverse (f .snd)
  Ī· = equivā†’unit (f .snd)
  Īµ = equivā†’counit (f .snd)
  zig = equivā†’zig (f .snd)
  zag = equivā†’zag (f .snd)

  injective : āˆ€ {x y} ā†’ to x ā‰” to y ā†’ x ā‰” y
  injective p = ap fst $ is-contrā†’is-prop (f .snd .is-eqv _) (_ , refl) (_ , sym p)

  injectiveā‚‚ : āˆ€ {x y z} ā†’ to x ā‰” z ā†’ to y ā‰” z ā†’ x ā‰” y
  injectiveā‚‚ p q = ap fst $ is-contrā†’is-prop (f .snd .is-eqv _)
    (_ , p) (_ , q)

  inverse : B ā‰ƒ A
  inverse = f eā»Ā¹

The proofs that equivalences are closed under composition assemble nicely into transitivity operators resembling equational reasoning:

_ā‰ƒāŸØ_āŸ©_ : āˆ€ {ā„“ ā„“ā‚ ā„“ā‚‚} (A : Type ā„“) {B : Type ā„“ā‚} {C : Type ā„“ā‚‚}
       ā†’ A ā‰ƒ B ā†’ B ā‰ƒ C ā†’ A ā‰ƒ C
A ā‰ƒāŸØ f āŸ©ā‰ƒ g = f āˆ™e g

_ā‰ƒāŸØāŸ©_ : āˆ€ {ā„“ ā„“ā‚} (A : Type ā„“) {B : Type ā„“ā‚} ā†’ A ā‰ƒ B ā†’ A ā‰ƒ B
x ā‰ƒāŸØāŸ© xā‰”y = xā‰”y

_ā‰ƒāˆŽ : āˆ€ {ā„“} (A : Type ā„“) ā†’ A ā‰ƒ A
x ā‰ƒāˆŽ = _ , id-equiv

infixr 2 _ā‰ƒāŸØāŸ©_ _ā‰ƒāŸØ_āŸ©_
infix  3 _ā‰ƒāˆŽ

Propositional ExtensionalityšŸ”—

The following observation is not very complex, but it is incredibly useful: Equivalence of propositions is the same as biimplication.

prop-ext : āˆ€ {ā„“ ā„“'} {P : Type ā„“} {Q : Type ā„“'}
         ā†’ is-prop P ā†’ is-prop Q
         ā†’ (P ā†’ Q) ā†’ (Q ā†’ P)
         ā†’ P ā‰ƒ Q
prop-ext pprop qprop pā†’q qā†’p .fst = pā†’q
prop-ext pprop qprop pā†’q qā†’p .snd .is-eqv y .centre = qā†’p y , qprop _ _
prop-ext pprop qprop pā†’q qā†’p .snd .is-eqv y .paths (p' , path) =
  Ī£-path (pprop _ _) (is-propā†’is-set qprop _ _ _ _)