------------------------------------------------------------------------
-- Weak equivalences
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

-- Partly based on Voevodsky's work on so-called univalent
-- foundations.

open import Equality

module Weak-equivalence
  {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

private
  module Bijection where
    import Bijection; open Bijection eq public
open Bijection hiding (id; _∘_; inverse)
open Derived-definitions-and-properties eq
import Groupoid; open Groupoid eq
open import Equivalence hiding (id; _∘_; inverse)
private
  module H-level where
    import H-level; open H-level eq public
open H-level
import H-level.Closure; open H-level.Closure eq
private
  module Injection where
    import Injection; open Injection eq public
open Injection using (_↣_; module _↣_; Injective)
private
  module Preimage where
    import Preimage; open Preimage eq public
open Preimage using (_⁻¹_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)
private
  module Surjection where
    import Surjection; open Surjection eq public
open Surjection using (_↠_; module _↠_)

------------------------------------------------------------------------
-- Is-weak-equivalence

-- A function f is a weak equivalence if all preimages under f are
-- contractible.

Is-weak-equivalence :  {a b} {A : Set a} {B : Set b} 
                      (A  B)  Set (a  b)
Is-weak-equivalence f =  y  Contractible (f ⁻¹ y)

abstract

  -- Is-weak-equivalence f is a proposition, assuming extensional
  -- equality.

  propositional :
     {a b} 
    ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
    {A : Set a} {B : Set b} (f : A  B) 
    Propositional (Is-weak-equivalence f)
  propositional {a} ext f =
    Π-closure (lower-extensionality a lzero ext) 1 λ _ 
      Contractible-propositional ext

-- Is-weak-equivalence respects extensional equality.

respects-extensional-equality :
   {a b} {A : Set a} {B : Set b} {f g : A  B} 
  (∀ x  f x  g x) 
  Is-weak-equivalence f  Is-weak-equivalence g
respects-extensional-equality f≡g f-weq = λ b 
  H-level.respects-surjection
    (_↔_.surjection (Preimage.respects-extensional-equality f≡g))
    0
    (f-weq b)

abstract

  -- The function subst is a weak equivalence family.
  --
  -- Note that this proof would be easier if subst P (refl x) p
  -- reduced to p.

  subst-is-weak-equivalence :
     {a p} {A : Set a} (P : A  Set p) {x y : A} (x≡y : x  y) 
    Is-weak-equivalence (subst P x≡y)
  subst-is-weak-equivalence P = elim
     {x y} x≡y  Is-weak-equivalence (subst P x≡y))
     x p  _ , λ q 
       (p , subst-refl P p)                                     ≡⟨ elim
                                                                      {u v : P x} u≡v 
                                                                        _≡_ {A =  λ (w : P x)  subst P (refl x) w  v}
                                                                            (v , subst-refl P v)
                                                                            (u , trans (subst-refl P u) u≡v))
                                                                      p  cong (_,_ p) (sym $ trans-reflʳ _))
                                                                     (proj₁ q                     ≡⟨ sym $ subst-refl P (proj₁ q) 
                                                                      subst P (refl x) (proj₁ q)  ≡⟨ proj₂ q ⟩∎
                                                                      p                           ) 
       (proj₁ q , (trans      (subst-refl P (proj₁ q))  $
                   trans (sym (subst-refl P (proj₁ q))) $
                         proj₂ q))                              ≡⟨ cong (_,_ (proj₁ q)) $ sym $ trans-assoc _ _ _ 
       (proj₁ q , trans (trans      (subst-refl P (proj₁ q))
                               (sym (subst-refl P (proj₁ q))))
                        (proj₂ q))                              ≡⟨ cong  eq  proj₁ q , trans eq (proj₂ q)) $ trans-symʳ _ 
       (proj₁ q , trans (refl _) (proj₂ q))                     ≡⟨ cong (_,_ (proj₁ q)) $ trans-reflˡ _ ⟩∎
       q                                                        )

  -- If Σ-map id f is a weak equivalence, then f is also a weak
  -- equivalence.

  drop-Σ-map-id :
     {a b} {A : Set a} {B C : A  Set b} (f :  {x}  B x  C x) 
    Is-weak-equivalence {A = Σ A B} {B = Σ A C} (Σ-map P.id f) 
     x  Is-weak-equivalence (f {x = x})
  drop-Σ-map-id {b = b} {A} {B} {C} f weq x z =
    H-level.respects-surjection surj 0 (weq (x , z))
    where
    map-f : Σ A B  Σ A C
    map-f = Σ-map P.id f

    to-P :  {x y} {p :  C}  (x , f y)  p  Set b
    to-P {y = y} {p} _ =  λ y′  f y′  proj₂ p

    to : map-f ⁻¹ (x , z)  f ⁻¹ z
    to ((x′ , y) , eq) = elim¹ to-P (y , refl (f y)) eq

    from : f ⁻¹ z  map-f ⁻¹ (x , z)
    from (y , eq) = (x , y) , cong (_,_ x) eq

    to∘from :  p  to (from p)  p
    to∘from (y , eq) = elim¹
       {z′} (eq : f y  z′) 
         _≡_ {A =  λ (y : B x)  f y  z′}
             (elim¹ to-P (y , refl (f y)) (cong (_,_ x) eq))
             (y , eq))
      (elim¹ to-P (y , refl (f y)) (cong (_,_ x) (refl (f y)))  ≡⟨ cong (elim¹ to-P (y , refl (f y))) $
                                                                        cong-refl (_,_ x) {x = f y} 
       elim¹ to-P (y , refl (f y)) (refl (x , f y))             ≡⟨ elim¹-refl to-P _ ⟩∎
       (y , refl (f y))                                         )
      eq

    surj : map-f ⁻¹ (x , z)  f ⁻¹ z
    surj = record
      { equivalence      = record { to = to; from = from }
      ; right-inverse-of = to∘from
      }

------------------------------------------------------------------------
-- _≈_

-- Weak equivalences.

infix 4 _≈_

record _≈_ {a b} (A : Set a) (B : Set b) : Set (a  b) where
  constructor weq
  field
    to                  : A  B
    is-weak-equivalence : Is-weak-equivalence to

  -- Weakly equivalent sets are isomorphic.

  from : B  A
  from = proj₁  proj₁  is-weak-equivalence

  abstract
    right-inverse-of :  x  to (from x)  x
    right-inverse-of = proj₂  proj₁  is-weak-equivalence

    left-inverse-of :  x  from (to x)  x
    left-inverse-of  = λ x 
      cong (proj₁ {B = λ x′  to x′  to x}) $
        proj₂ (is-weak-equivalence (to x)) (x , refl (to x))

  bijection : A  B
  bijection = record
    { surjection = record
      { equivalence = record
        { to   = to
        ; from = from
        }
      ; right-inverse-of = right-inverse-of
      }
    ; left-inverse-of = left-inverse-of
    }

  open _↔_ bijection public
    hiding (from; to; right-inverse-of; left-inverse-of)

  abstract

    -- All preimages of an element under the weak equivalence are
    -- equal.

    irrelevance :  y (p : to ⁻¹ y)  (from y , right-inverse-of y)  p
    irrelevance = proj₂  is-weak-equivalence

    -- The two proofs left-inverse-of and right-inverse-of are
    -- related.

    left-right-lemma :
       x  cong to (left-inverse-of x)  right-inverse-of (to x)
    left-right-lemma x =
      lemma₁ to _ _ (lemma₂ (irrelevance (to x) (x , refl (to x))))
      where
      lemma₁ : {x y : A} (f : A  B) (p : x  y) (q : f x  f y) 
               refl (f y)  trans (cong f (sym p)) q 
               cong f p  q
      lemma₁ f = elim
         {x y} p   q  refl (f y)  trans (cong f (sym p)) q 
                           cong f p  q)
         x q hyp 
           cong f (refl x)                  ≡⟨ cong-refl f 
           refl (f x)                       ≡⟨ hyp 
           trans (cong f (sym (refl x))) q  ≡⟨ cong  p  trans (cong f p) q) sym-refl 
           trans (cong f (refl x)) q        ≡⟨ cong  p  trans p q) (cong-refl f) 
           trans (refl (f x)) q             ≡⟨ trans-reflˡ _ ⟩∎
           q                                )

      lemma₂ :  {f : A  B} {y} {f⁻¹y₁ f⁻¹y₂ : f ⁻¹ y}
               (p : f⁻¹y₁  f⁻¹y₂) 
               proj₂ f⁻¹y₂ 
               trans (cong f (sym (cong (proj₁ {B = λ x  f x  y}) p)))
                     (proj₂ f⁻¹y₁)
      lemma₂ {f} {y} =
        let pr = proj₁ {B = λ x  f x  y} in
        elim {A = f ⁻¹ y}
           {f⁻¹y₁ f⁻¹y₂} p 
             proj₂ f⁻¹y₂ 
               trans (cong f (sym (cong pr p))) (proj₂ f⁻¹y₁))
           f⁻¹y 
             proj₂ f⁻¹y                                               ≡⟨ sym $ trans-reflˡ _ 
             trans (refl (f (proj₁ f⁻¹y))) (proj₂ f⁻¹y)               ≡⟨ cong  p  trans p (proj₂ f⁻¹y)) (sym (cong-refl f)) 
             trans (cong f (refl (proj₁ f⁻¹y))) (proj₂ f⁻¹y)          ≡⟨ cong  p  trans (cong f p) (proj₂ f⁻¹y)) (sym sym-refl) 
             trans (cong f (sym (refl (proj₁ f⁻¹y)))) (proj₂ f⁻¹y)    ≡⟨ cong  p  trans (cong f (sym p)) (proj₂ f⁻¹y))
                                                                              (sym (cong-refl pr)) ⟩∎
             trans (cong f (sym (cong pr (refl f⁻¹y)))) (proj₂ f⁻¹y)  )

-- Bijections are weak equivalences.

bijection⇒weak-equivalence :  {a b} {A : Set a} {B : Set b} 
                             A  B  A  B
bijection⇒weak-equivalence A↔B = record
  { to                  = to
  ; is-weak-equivalence = λ y 
      (from y , right-inverse-of y) , irrelevance y
  }
  where
  open _↔_ A↔B using (to; from)

  abstract
    is-weak-equivalence : Is-weak-equivalence to
    is-weak-equivalence = Preimage.bijection⁻¹-contractible A↔B

    right-inverse-of :  x  to (from x)  x
    right-inverse-of = proj₂  proj₁  is-weak-equivalence

    irrelevance :  y (p : to ⁻¹ y)  (from y , right-inverse-of y)  p
    irrelevance = proj₂  is-weak-equivalence

------------------------------------------------------------------------
-- Equivalence

-- Weak equivalences are equivalence relations.

id :  {a} {A : Set a}  A  A
id {A = A} = record
  { to                  = to
  ; is-weak-equivalence = λ y 
      (from y , right-inverse-of y) , irrelevance y
  }
  where
  A≈A  = bijection⇒weak-equivalence (Bijection.id {A = A})
  to   = _≈_.to   A≈A
  from = _≈_.from A≈A

  abstract
    right-inverse-of :  x  to (from x)  x
    right-inverse-of = _≈_.right-inverse-of A≈A

    irrelevance :  y (p : to ⁻¹ y)  (from y , right-inverse-of y)  p
    irrelevance = _≈_.irrelevance A≈A

inverse :  {a b} {A : Set a} {B : Set b}  A  B  B  A
inverse A≈B = record
  { to                  = to
  ; is-weak-equivalence = λ y 
      (from y , right-inverse-of y) , irrelevance y
  }
  where
  B≈A  = bijection⇒weak-equivalence $
         Bijection.inverse $
         _≈_.bijection A≈B
  to   = _≈_.to   B≈A
  from = _≈_.from B≈A

  abstract
    right-inverse-of :  x  to (from x)  x
    right-inverse-of = _≈_.right-inverse-of B≈A

    irrelevance :  y (p : to ⁻¹ y)  (from y , right-inverse-of y)  p
    irrelevance = _≈_.irrelevance B≈A

infixr 9 _∘_

_∘_ :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
      B  C  A  B  A  C
f  g = record
  { to                  = to
  ; is-weak-equivalence = λ y 
      (from y , right-inverse-of y) , irrelevance y
  }
  where
  f∘g  = bijection⇒weak-equivalence $
         Bijection._∘_ (_≈_.bijection f) (_≈_.bijection g)
  to   = _≈_.to   f∘g
  from = _≈_.from f∘g

  abstract
    right-inverse-of :  x  to (from x)  x
    right-inverse-of = _≈_.right-inverse-of f∘g

    irrelevance :  y (p : to ⁻¹ y)  (from y , right-inverse-of y)  p
    irrelevance = _≈_.irrelevance f∘g

-- Equational reasoning combinators.

infixr 0 _≈⟨_⟩_
infix  0 finally-≈

_≈⟨_⟩_ :  {a b c} (A : Set a) {B : Set b} {C : Set c} 
         A  B  B  C  A  C
_ ≈⟨ A≈B  B≈C = B≈C  A≈B

finally-≈ :  {a b} (A : Set a) (B : Set b)  A  B  A  B
finally-≈ _ _ A≈B = A≈B

syntax finally-≈ A B A≈B = A ≈⟨ A≈B ⟩□ B □

------------------------------------------------------------------------
-- The two-out-of-three property

-- If two out of three of f, g and g ∘ f are weak equivalences, then
-- the third one is also a weak equivalence.

record Two-out-of-three
         {a b c} {A : Set a} {B : Set b} {C : Set c}
         (f : A  B) (g : B  C) : Set (a  b  c) where
  field
    f-g   : Is-weak-equivalence f  Is-weak-equivalence g 
            Is-weak-equivalence (g  f)
    g-g∘f : Is-weak-equivalence g  Is-weak-equivalence (g  f) 
            Is-weak-equivalence f
    g∘f-f : Is-weak-equivalence (g  f)  Is-weak-equivalence f 
            Is-weak-equivalence g

two-out-of-three :
   {a b c} {A : Set a} {B : Set b} {C : Set c}
  (f : A  B) (g : B  C)  Two-out-of-three f g
two-out-of-three f g = record
  { f-g   = λ f-weq g-weq 
              _≈_.is-weak-equivalence (weq g g-weq  weq f f-weq)
  ; g-g∘f = λ g-weq g∘f-weq 
              respects-extensional-equality
                 x  let g⁻¹ = _≈_.from (weq g g-weq) in
                   g⁻¹ (g (f x))  ≡⟨ _≈_.left-inverse-of (weq g g-weq) (f x) ⟩∎
                   f x            )
                (_≈_.is-weak-equivalence
                   (inverse (weq g g-weq)  weq _ g∘f-weq))
  ; g∘f-f = λ g∘f-weq f-weq 
              respects-extensional-equality
                 x  let f⁻¹ = _≈_.from (weq f f-weq) in
                   g (f (f⁻¹ x))  ≡⟨ cong g (_≈_.right-inverse-of (weq f f-weq) x) ⟩∎
                   g x            )
                (_≈_.is-weak-equivalence
                   (weq _ g∘f-weq  inverse (weq f f-weq)))
  }

------------------------------------------------------------------------
-- f ≡ g and ∀ x → f x ≡ g x are isomorphic (assuming extensionality)

abstract

  -- Functions between contractible types are weak equivalences.

  function-between-contractible-types-is-weak-equivalence :
     {a b} {A : Set a} {B : Set b} (f : A  B) 
    Contractible A  Contractible B  Is-weak-equivalence f
  function-between-contractible-types-is-weak-equivalence f cA cB =
    Two-out-of-three.g-g∘f
      (two-out-of-three f (const tt))
      (lemma cB)
      (lemma cA)
    where
    -- Functions from a contractible type to the unit type are
    -- contractible.

    lemma :  {b} {C : Set b}  Contractible C 
            Is-weak-equivalence  (_ : C)  tt)
    lemma (x , irr) _ = (x , refl tt) , λ p 
      (x , refl tt)  ≡⟨ _↔_.to Σ-≡,≡↔≡ (irr (proj₁ p) ,
                          (subst  _  tt  tt)
                             (irr (proj₁ p)) (refl tt)  ≡⟨ elim  eq  subst  _  tt  tt) eq (refl tt)  refl tt)
                                                                 _  subst-refl  _  tt  tt) (refl tt))
                                                                (irr (proj₁ p)) 
                           refl tt                      ≡⟨ elim  eq  refl tt  eq) (refl  refl) (proj₂ p) ⟩∎
                           proj₂ p                      )) ⟩∎
      p              

  -- ext⁻¹ is a weak equivalence (assuming extensionality).

  ext⁻¹-is-weak-equivalence :
     {a b} {A : Set a} 
    ({B : A  Set b}  Extensionality A B) 
    {B : A  Set b} {f g : (x : A)  B x} 
    Is-weak-equivalence (ext⁻¹ {f = f} {g = g})
  ext⁻¹-is-weak-equivalence ext {f = f} {g} =
    let surj : (∀ x  Singleton (g x))  ( λ f   x  f x  g x)
        surj = record
          { equivalence = record
            { to   = λ f  proj₁  f , proj₂  f
            ; from = λ p x  proj₁ p x , proj₂ p x
            }
          ; right-inverse-of = refl
          }

        lemma₁ : Contractible ( λ f   x  f x  g x)
        lemma₁ =
          H-level.respects-surjection surj 0 $
            _⇔_.from Π-closure-contractible⇔extensionality
              ext (singleton-contractible  g)

        lemma₂ : Is-weak-equivalence (Σ-map P.id ext⁻¹)
        lemma₂ = function-between-contractible-types-is-weak-equivalence
                   _ (singleton-contractible g) lemma₁

    in drop-Σ-map-id ext⁻¹ lemma₂ f

-- f ≡ g and ∀ x → f x ≡ g x are isomorphic (assuming extensionality).

extensionality-isomorphism :
   {a b} {A : Set a} 
  ({B : A  Set b}  Extensionality A B) 
  {B : A  Set b} {f g : (x : A)  B x} 
  (∀ x  f x  g x)  (f  g)
extensionality-isomorphism ext =
  inverse (weq _ (ext⁻¹-is-weak-equivalence ext))

------------------------------------------------------------------------
-- Groupoid

abstract

  -- Two proofs of weak equivalence are equal if the function
  -- components are equal (assuming extensionality).

  lift-equality :
     {a b} 
    ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
    {A : Set a} {B : Set b} {p q : A  B} 
    (∀ x  _≈_.to p x  _≈_.to q x)  p  q
  lift-equality {a} {b} ext {p = weq f f-weq} {q = weq g g-weq} f≡g =
    elim  {f g} f≡g   f-weq g-weq  weq f f-weq  weq g g-weq)
          f f-weq g-weq 
            cong (weq f)
              (_⇔_.to {To = Proof-irrelevant _}
                      propositional⇔irrelevant
                      (propositional ext f) f-weq g-weq))
         (lower-extensionality b a ext f≡g)
         f-weq g-weq

-- _≈_ comes with a groupoid structure (assuming extensionality).

groupoid :  {} 
           ({A : Set } {B : A  Set }  Extensionality A B) 
           Groupoid (lsuc ) 
groupoid {} ext = record
  { Object         = Set 
  ; _∼_            = _≈_
  ; id             = id
  ; _∘_            = _∘_
  ; _⁻¹            = inverse
  ; left-identity  = left-identity
  ; right-identity = right-identity
  ; assoc          = assoc
  ; left-inverse   = left-inverse
  ; right-inverse  = right-inverse
  }
  where
  abstract
    left-identity : {X Y : Set } (p : X  Y)  id  p  p
    left-identity _ = lift-equality ext  _  refl _)

    right-identity : {X Y : Set } (p : X  Y)  p  id  p
    right-identity _ = lift-equality ext  _  refl _)

    assoc : {W X Y Z : Set } (p : Y  Z) (q : X  Y) (r : W  X) 
            p  (q  r)  (p  q)  r
    assoc _ _ _ = lift-equality ext  _  refl _)

    left-inverse : {X Y : Set } (p : X  Y)  inverse p  p  id
    left-inverse p = lift-equality ext (_≈_.left-inverse-of p)

    right-inverse : {X Y : Set } (p : X  Y)  p  inverse p  id
    right-inverse p = lift-equality ext (_≈_.right-inverse-of p)

------------------------------------------------------------------------
-- A surjection from A ↔ B to A ≈ B

abstract

  -- bijection⇒weak-equivalence is a left inverse of _≈_.bijection
  -- (assuming extensionality).

  bijection⇒weak-equivalence-left-inverse :
     {a b} {A : Set a} {B : Set b} 
    ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
    (A≈B : A  B) 
    bijection⇒weak-equivalence (_≈_.bijection A≈B)  A≈B
  bijection⇒weak-equivalence-left-inverse ext _ =
    lift-equality ext  _  refl _)

  -- When sets are used bijection⇒weak-equivalence is a right inverse
  -- of _≈_.bijection (assuming extensionality).

  bijection⇒weak-equivalence-right-inverse :
     {a b} {A : Set a} {B : Set b} 
    ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
    Is-set A  (A↔B : A  B) 
    _≈_.bijection (bijection⇒weak-equivalence A↔B)  A↔B
  bijection⇒weak-equivalence-right-inverse {a} {b} {B = B}
                                           ext A-set A↔B =
    cong₂  l r  record
             { surjection = record
               { equivalence      = _↔_.equivalence A↔B
               ; right-inverse-of = r
               }
             ; left-inverse-of = l
             })
          (lower-extensionality b b ext λ _  _⇔_.to set⇔UIP A-set _ _)
          (lower-extensionality a a ext λ _  _⇔_.to set⇔UIP B-set _ _)
    where
    B-set : Is-set B
    B-set = respects-surjection (_↔_.surjection A↔B) 2 A-set

-- There is a surjection from A ↔ B to A ≈ B (assuming
-- extensionality).

↔-↠-≈ :
   {a b} {A : Set a} {B : Set b} 
  ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
  (A  B)  (A  B)
↔-↠-≈ ext = record
  { equivalence = record
    { to   = bijection⇒weak-equivalence
    ; from = _≈_.bijection
    }
  ; right-inverse-of = bijection⇒weak-equivalence-left-inverse ext
  }

-- When A is a set A ↔ B and A ≈ B are isomorphic (assuming
-- extensionality).

↔-↔-≈ :
   {a b} {A : Set a} {B : Set b} 
  ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
  Is-set A  (A  B)  (A  B)
↔-↔-≈ ext A-set = record
  { surjection      = ↔-↠-≈ ext
  ; left-inverse-of = bijection⇒weak-equivalence-right-inverse ext A-set
  }

------------------------------------------------------------------------
-- Closure, preservation

abstract

  -- Positive h-levels are closed under the weak equivalence operator
  -- (assuming extensionality).

  right-closure :
     {a b} 
    ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
     {A : Set a} {B : Set b} n 
    H-level (1 + n) B  H-level (1 + n) (A  B)
  right-closure {a} {b} ext {A = A} {B} n h =
    H-level.respects-surjection surj (1 + n) lemma
    where
    lemma : H-level (1 + n) ( λ (to : A  B)  Is-weak-equivalence to)
    lemma = Σ-closure (1 + n)
              (Π-closure (lower-extensionality b a ext)
                         (1 + n) (const h))
              (mono (m≤m+n 1 n)  propositional ext)

    surj : ( λ (to : A  B)  Is-weak-equivalence to)  (A  B)
    surj = record
      { equivalence = record
          { to   = λ A≈B  weq (proj₁ A≈B) (proj₂ A≈B)
          ; from = λ A≈B  (_≈_.to A≈B , _≈_.is-weak-equivalence A≈B)
          }
      ; right-inverse-of = λ _  refl _
      }

  left-closure :
     {a b} 
    ({A : Set (a  b)} {B : A  Set (a  b)}  Extensionality A B) 
     {A : Set a} {B : Set b} n 
    H-level (1 + n) A  H-level (1 + n) (A  B)
  left-closure ext {A = A} {B} n h =
    H-level.[inhabited⇒+]⇒+ n λ (A≈B : A  B) 
      right-closure ext n $
        H-level.respects-surjection (_≈_.surjection A≈B) (1 + n) h

-- Equalities are closed, in a strong sense, under applications of
-- weak equivalences.

≈-≡ :  {a b} {A : Set a} {B : Set b} (A≈B : A  B) {x y : A} 
      let open _≈_ A≈B in
      (to x  to y)  (x  y)
≈-≡ A≈B {x} {y} =
  bijection⇒weak-equivalence record
    { surjection      = surjection′
    ; left-inverse-of = left-inverse-of′
    }
  where
  open _≈_ A≈B

  surjection′ : (to x  to y)  (x  y)
  surjection′ =
    Surjection.↠-≡ $
    _↔_.surjection $
    Bijection.inverse $
    _≈_.bijection A≈B

  abstract
    left-inverse-of′ :
       p  _↠_.from surjection′ (_↠_.to surjection′ p)  p
    left-inverse-of′ = λ to-x≡to-y 
      cong to (
        trans (sym (left-inverse-of x)) $
        trans (cong from to-x≡to-y) $
        left-inverse-of y)                         ≡⟨ cong-trans to _ _ 
      trans (cong to (sym (left-inverse-of x))) (
        cong to (trans (cong from to-x≡to-y) (
                 left-inverse-of y)))              ≡⟨ cong₂ trans (cong-sym to _) (cong-trans to _ _) 
      trans (sym (cong to (left-inverse-of x))) (
        trans (cong to (cong from to-x≡to-y)) (
        cong to (left-inverse-of y)))              ≡⟨ cong₂  eq₁ eq₂  trans (sym eq₁) $
                                                                         trans (cong to (cong from to-x≡to-y)) $
                                                                         eq₂)
                                                           (left-right-lemma x)
                                                           (left-right-lemma y) 
      trans (sym (right-inverse-of (to x))) (
        trans (cong to (cong from to-x≡to-y)) (
        right-inverse-of (to y)))                  ≡⟨ _↠_.right-inverse-of (Surjection.↠-≡ $ _≈_.surjection A≈B) to-x≡to-y ⟩∎
      to-x≡to-y                                    

abstract
  private

    -- We can push subst through certain function applications.

    push-subst :
       {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
        (B₁ : A₁  Set b₁) {B₂ : A₂  Set b₂}
        {f : A₂  A₁} {x₁ x₂ : A₂} {y : B₁ (f x₁)}
      (g :  x  B₁ (f x)  B₂ x) (eq : x₁  x₂) 
      subst B₂ eq (g x₁ y)  g x₂ (subst B₁ (cong f eq) y)
    push-subst B₁ {B₂} {f} g eq = elim
       {x₁ x₂} eq   y  subst B₂ eq (g x₁ y) 
                            g x₂ (subst B₁ (cong f eq) y))
       x y  subst B₂ (refl x) (g x y)           ≡⟨ subst-refl B₂ _ 
               g x y                               ≡⟨ sym $ cong (g x) $ subst-refl B₁ _ 
               g x (subst B₁ (refl (f x)) y)       ≡⟨ cong  eq  g x (subst B₁ eq y)) (sym $ cong-refl f) ⟩∎
               g x (subst B₁ (cong f (refl x)) y)  )
      eq _

    push-subst′ :
       {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
      (A₁≈A₂ : A₁  A₂) (B₁ : A₁  Set b₁) (B₂ : A₂  Set b₂) 
      let open _≈_ A₁≈A₂ in {x₁ x₂ : A₁} {y : B₁ (from (to x₁))}
      (g :  x  B₁ (from (to x))  B₂ (to x)) (eq : to x₁  to x₂) 
      subst B₂ eq (g x₁ y)  g x₂ (subst B₁ (cong from eq) y)
    push-subst′ A₁≈A₂ B₁ B₂ {x₁} {x₂} {y} g eq =
      subst B₂ eq (g x₁ y)                    ≡⟨ cong (subst B₂ eq) $ sym $ g′-lemma _ _ 
      subst B₂ eq (g′ (to x₁) y)              ≡⟨ push-subst B₁ g′ eq 
      g′ (to x₂) (subst B₁ (cong from eq) y)  ≡⟨ g′-lemma _ _ ⟩∎
      g x₂ (subst B₁ (cong from eq) y)        
      where
      open _≈_ A₁≈A₂

      g′ :  x′  B₁ (from x′)  B₂ x′
      g′ x′ y = subst B₂ (right-inverse-of x′) $
                g (from x′) $
                subst B₁ (sym $ cong from $ right-inverse-of x′) y

      g′-lemma :  x y  g′ (to x) y  g x y
      g′-lemma x y =
        let lemma = λ y 
              let gy = g (from (to x)) $
                         subst B₁
                           (sym $ cong from $ cong to (refl _)) y in
              subst B₂ (cong to (refl _)) gy             ≡⟨ cong  p  subst B₂ p gy) $ cong-refl to 
              subst B₂ (refl _) gy                       ≡⟨ subst-refl B₂ gy 
              gy                                         ≡⟨ cong  p  g (from (to x)) $ subst B₁ (sym $ cong from p) y) $ cong-refl to 
              g (from (to x))
                (subst B₁ (sym $ cong from (refl _)) y)  ≡⟨ cong  p  g (from (to x)) $ subst B₁ (sym p) y) $ cong-refl from 
              g (from (to x))
                (subst B₁ (sym (refl _)) y)              ≡⟨ cong  p  g (from (to x)) $ subst B₁ p y) sym-refl 
              g (from (to x)) (subst B₁ (refl _) y)      ≡⟨ cong (g (from (to x))) $ subst-refl B₁ y ⟩∎
              g (from (to x)) y                          
        in
        subst B₂ (right-inverse-of (to x))
          (g (from (to x)) $
           subst B₁ (sym $ cong from $
                       right-inverse-of (to x)) y)  ≡⟨ cong  p  subst B₂ p (g (from (to x)) $ subst B₁ (sym $ cong from p) y)) $
                                                         sym $ left-right-lemma x 
        subst B₂ (cong to $ left-inverse-of x)
          (g (from (to x)) $
           subst B₁ (sym $ cong from $ cong to $
                       left-inverse-of x) y)        ≡⟨ elim¹
                                                          {x′} eq 
                                                            (y : B₁ (from (to x′))) 
                                                            subst B₂ (cong to eq)
                                                              (g (from (to x)) $ subst B₁ (sym $ cong from $ cong to eq) y) 
                                                            g x′ y)
                                                         lemma
                                                         (left-inverse-of x) y ⟩∎
        g x y                                       

-- If the first component is instantiated to id, then the following
-- lemmas state that ∃ preserves functions, equivalences, injections,
-- surjections and bijections.

∃-preserves-functions :
   {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂}
  (A₁≈A₂ : A₁  A₂)  (∀ x  B₁ x  B₂ (_≈_.to A₁≈A₂ x)) 
  Σ A₁ B₁  Σ A₂ B₂
∃-preserves-functions A₁≈A₂ B₁→B₂ = Σ-map (_≈_.to A₁≈A₂) (B₁→B₂ _)

∃-preserves-equivalences :
   {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂}
  (A₁≈A₂ : A₁  A₂)  (∀ x  B₁ x  B₂ (_≈_.to A₁≈A₂ x)) 
  Σ A₁ B₁  Σ A₂ B₂
∃-preserves-equivalences {B₂ = B₂} A₁≈A₂ B₁⇔B₂ = record
  { to   = ∃-preserves-functions A₁≈A₂ (_⇔_.to  B₁⇔B₂)
  ; from =
     ∃-preserves-functions
       (inverse A₁≈A₂)
        x y  _⇔_.from
                  (B₁⇔B₂ (_≈_.from A₁≈A₂ x))
                  (subst B₂ (sym (_≈_.right-inverse-of A₁≈A₂ x)) y))
  }

∃-preserves-injections :
   {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂}
  (A₁≈A₂ : A₁  A₂)  (∀ x  B₁ x  B₂ (_≈_.to A₁≈A₂ x)) 
  Σ A₁ B₁  Σ A₂ B₂
∃-preserves-injections {A₁ = A₁} {A₂} {B₁} {B₂} A₁≈A₂ B₁↣B₂ = record
  { to        = to′
  ; injective = injective′
  }
  where
  open _↣_

  to′ : Σ A₁ B₁  Σ A₂ B₂
  to′ = ∃-preserves-functions A₁≈A₂ (_↣_.to  B₁↣B₂)

  abstract
    injective′ : Injective to′
    injective′ {x = (x₁ , x₂)} {y = (y₁ , y₂)} =
      _↔_.to Σ-≡,≡↔≡ 
      Σ-map (_≈_.injective A₁≈A₂)  {eq₁} eq₂ 
        let lemma =
              to (B₁↣B₂ y₁) (subst B₁ (_≈_.injective A₁≈A₂ eq₁) x₂)      ≡⟨ refl _ 
              to (B₁↣B₂ y₁)
                (subst B₁ (trans (sym (_≈_.left-inverse-of A₁≈A₂ x₁)) $
                           trans (cong (_≈_.from A₁≈A₂) eq₁)
                                 (_≈_.left-inverse-of A₁≈A₂ y₁))
                          x₂)                                            ≡⟨ cong (to (B₁↣B₂ y₁)) $ sym $ subst-subst B₁ _ _ _ 
              to (B₁↣B₂ y₁)
                 (subst B₁ (trans (cong (_≈_.from A₁≈A₂) eq₁)
                                  (_≈_.left-inverse-of A₁≈A₂ y₁)) $
                  subst B₁ (sym (_≈_.left-inverse-of A₁≈A₂ x₁))
                           x₂)                                           ≡⟨ cong (to (B₁↣B₂ y₁)) $ sym $ subst-subst B₁ _ _ _ 
              to (B₁↣B₂ y₁)
                 (subst B₁ (_≈_.left-inverse-of A₁≈A₂ y₁) $
                  subst B₁ (cong (_≈_.from A₁≈A₂) eq₁) $
                  subst B₁ (sym (_≈_.left-inverse-of A₁≈A₂ x₁)) x₂)      ≡⟨ sym $ push-subst′ A₁≈A₂ B₁ B₂
                                                                               x y  to (B₁↣B₂ x)
                                                                                          (subst B₁ (_≈_.left-inverse-of A₁≈A₂ x) y))
                                                                              eq₁ 
              subst B₂ eq₁
                (to (B₁↣B₂ x₁) $
                 subst B₁ (_≈_.left-inverse-of A₁≈A₂ x₁) $
                 subst B₁ (sym (_≈_.left-inverse-of A₁≈A₂ x₁)) x₂)       ≡⟨ cong (subst B₂ eq₁  to (B₁↣B₂ x₁)) $ subst-subst B₁ _ _ _ 
              subst B₂ eq₁
                (to (B₁↣B₂ x₁) $
                 subst B₁ (trans (sym (_≈_.left-inverse-of A₁≈A₂ x₁))
                                 (_≈_.left-inverse-of A₁≈A₂ x₁))
                          x₂)                                            ≡⟨ cong  p  subst B₂ eq₁ (to (B₁↣B₂ x₁) (subst B₁ p x₂))) $
                                                                                 trans-symˡ _ 
              subst B₂ eq₁ (to (B₁↣B₂ x₁) $ subst B₁ (refl _) x₂)        ≡⟨ cong (subst B₂ eq₁  to (B₁↣B₂ x₁)) $
                                                                                 subst-refl B₁ x₂ 
              subst B₂ eq₁ (to (B₁↣B₂ x₁) x₂)                            ≡⟨ eq₂ ⟩∎
              to (B₁↣B₂ y₁) y₂                                           
        in
        subst B₁ (_≈_.injective A₁≈A₂ eq₁) x₂  ≡⟨ _↣_.injective (B₁↣B₂ y₁) lemma ⟩∎
        y₂                                     ) 
      _↔_.from Σ-≡,≡↔≡

∃-preserves-surjections :
   {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂}
  (A₁≈A₂ : A₁  A₂)  (∀ x  B₁ x  B₂ (_≈_.to A₁≈A₂ x)) 
  Σ A₁ B₁  Σ A₂ B₂
∃-preserves-surjections {A₁ = A₁} {A₂} {B₁} {B₂} A₁≈A₂ B₁↠B₂ = record
  { equivalence      = equivalence′
  ; right-inverse-of = right-inverse-of′
  }
  where
  open _↠_

  equivalence′ : Σ A₁ B₁  Σ A₂ B₂
  equivalence′ = ∃-preserves-equivalences A₁≈A₂ (equivalence  B₁↠B₂)

  abstract
    right-inverse-of′ :
       p  _⇔_.to equivalence′ (_⇔_.from equivalence′ p)  p
    right-inverse-of′ = λ p  _↔_.to Σ-≡,≡↔≡
      ( _≈_.right-inverse-of A₁≈A₂ (proj₁ p)
      , (subst B₂ (_≈_.right-inverse-of A₁≈A₂ (proj₁ p))
           (to (B₁↠B₂ _) (from (B₁↠B₂ _)
              (subst B₂ (sym (_≈_.right-inverse-of A₁≈A₂ (proj₁ p)))
                 (proj₂ p))))                                         ≡⟨ cong (subst B₂ _) $ right-inverse-of (B₁↠B₂ _) _ 
         subst B₂ (_≈_.right-inverse-of A₁≈A₂ (proj₁ p))
           (subst B₂ (sym (_≈_.right-inverse-of A₁≈A₂ (proj₁ p)))
              (proj₂ p))                                              ≡⟨ subst-subst-sym B₂ _ _ ⟩∎
         proj₂ p )
      )

∃-preserves-bijections :
   {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂}
  (A₁≈A₂ : A₁  A₂)  (∀ x  B₁ x  B₂ (_≈_.to A₁≈A₂ x)) 
  Σ A₁ B₁  Σ A₂ B₂
∃-preserves-bijections {A₁ = A₁} {A₂} {B₁} {B₂} A₁≈A₂ B₁↔B₂ = record
  { surjection      = surjection′
  ; left-inverse-of = left-inverse-of′
  }
  where
  open _↔_

  surjection′ : Σ A₁ B₁  Σ A₂ B₂
  surjection′ = ∃-preserves-surjections A₁≈A₂ (surjection  B₁↔B₂)

  abstract
    left-inverse-of′ :
       p  _↠_.from surjection′ (_↠_.to surjection′ p)  p
    left-inverse-of′ = λ p  _↔_.to Σ-≡,≡↔≡
      ( _≈_.left-inverse-of A₁≈A₂ (proj₁ p)
      , (subst B₁ (_≈_.left-inverse-of A₁≈A₂ (proj₁ p))
           (from (B₁↔B₂ _)
              (subst B₂ (sym (_≈_.right-inverse-of A₁≈A₂
                                (_≈_.to A₁≈A₂ (proj₁ p))))
                 (to (B₁↔B₂ _) (proj₂ p))))                        ≡⟨ push-subst B₂  x  from (B₁↔B₂ x))
                                                                        (_≈_.left-inverse-of A₁≈A₂ (proj₁ p)) 
         from (B₁↔B₂ _)
           (subst B₂ (cong (_≈_.to A₁≈A₂)
                           (_≈_.left-inverse-of A₁≈A₂ (proj₁ p)))
              (subst B₂ (sym (_≈_.right-inverse-of A₁≈A₂
                                (_≈_.to A₁≈A₂ (proj₁ p))))
                 (to (B₁↔B₂ _) (proj₂ p))))                        ≡⟨ cong  eq  from (B₁↔B₂ _)
                                                                                     (subst B₂ eq
                                                                                        (subst B₂ (sym (_≈_.right-inverse-of A₁≈A₂ _))
                                                                                           (to (B₁↔B₂ _) (proj₂ p))))) $
                                                                           _≈_.left-right-lemma A₁≈A₂ _ 
         from (B₁↔B₂ _)
           (subst B₂ (_≈_.right-inverse-of A₁≈A₂
                        (_≈_.to A₁≈A₂ (proj₁ p)))
              (subst B₂ (sym (_≈_.right-inverse-of A₁≈A₂
                                (_≈_.to A₁≈A₂ (proj₁ p))))
                 (to (B₁↔B₂ _) (proj₂ p))))                        ≡⟨ cong (from (B₁↔B₂ _)) $ subst-subst-sym B₂ _ _ 
         from (B₁↔B₂ _) (to (B₁↔B₂ _) (proj₂ p))                   ≡⟨ left-inverse-of (B₁↔B₂ _) _ ⟩∎
         proj₂ p                                                   )
      )

-- Σ preserves weak equivalence.

Σ-preserves :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂}
              (A₁≈A₂ : A₁  A₂)  (∀ x  B₁ x  B₂ (_≈_.to A₁≈A₂ x)) 
              Σ A₁ B₁  Σ A₂ B₂
Σ-preserves A₁≈A₂ B₁≈B₂ = bijection⇒weak-equivalence $
  ∃-preserves-bijections A₁≈A₂ (_≈_.bijection  B₁≈B₂)

-- Π preserves weak equivalence (assuming extensionality).

Π-preserves :
   {a₁ a₂ b₁ b₂} 
  ({A : Set (a₁  a₂)} {B : A  Set (b₁  b₂)}  Extensionality A B) 
  {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
  (A₁≈A₂ : A₁  A₂)  (∀ x  B₁ x  B₂ (_≈_.to A₁≈A₂ x)) 
  ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
Π-preserves {a₁} {a₂} {b₁} {b₂} ext
            {A₁ = A₁} {A₂} {B₁} {B₂} A₁≈A₂ B₁≈B₂ =
  bijection⇒weak-equivalence record
    { surjection = record
      { equivalence = record
        { to   = to′
        ; from = from′
        }
      ; right-inverse-of = right-inverse-of′
      }
    ; left-inverse-of = left-inverse-of′
    }
  where
  open _≈_

  to′ : ((x : A₁)  B₁ x)  (x : A₂)  B₂ x
  to′ f x = subst B₂ (right-inverse-of A₁≈A₂ x)
                  (to (B₁≈B₂ (from A₁≈A₂ x))
                      (f (from A₁≈A₂ x)))

  from′ : ((x : A₂)  B₂ x)  (x : A₁)  B₁ x
  from′ f x = from (B₁≈B₂ x) (f (to A₁≈A₂ x))

  abstract
    right-inverse-of′ :  f  to′ (from′ f)  f
    right-inverse-of′ = λ f  lower-extensionality a₁ b₁ ext λ x 
      subst B₂ (right-inverse-of A₁≈A₂ x)
            (to (B₁≈B₂ (from A₁≈A₂ x))
                (from (B₁≈B₂ (from A₁≈A₂ x))
                      (f (to A₁≈A₂ (from A₁≈A₂ x)))))  ≡⟨ cong (subst B₂ (right-inverse-of A₁≈A₂ x)) $
                                                               right-inverse-of (B₁≈B₂ _) _ 
      subst B₂ (right-inverse-of A₁≈A₂ x)
            (f (to A₁≈A₂ (from A₁≈A₂ x)))              ≡⟨ elim  {x y} x≡y  subst B₂ x≡y (f x)  f y)
                                                                x  subst-refl B₂ (f x))
                                                               (right-inverse-of A₁≈A₂ x) ⟩∎
      f x                                              

    left-inverse-of′ :  f  from′ (to′ f)  f
    left-inverse-of′ = λ f  lower-extensionality a₂ b₂ ext λ x 
      from (B₁≈B₂ x)
           (subst B₂ (right-inverse-of A₁≈A₂ (to A₁≈A₂ x))
                  (to (B₁≈B₂ (from A₁≈A₂ (to A₁≈A₂ x)))
                      (f (from A₁≈A₂ (to A₁≈A₂ x)))))             ≡⟨ cong  eq  from (B₁≈B₂ x)
                                                                                    (subst B₂ eq
                                                                                       (to (B₁≈B₂ (from A₁≈A₂ (to A₁≈A₂ x)))
                                                                                          (f (from A₁≈A₂ (to A₁≈A₂ x))))))
                                                                          (sym $ left-right-lemma A₁≈A₂ x) 
      from (B₁≈B₂ x)
           (subst B₂ (cong (to A₁≈A₂) (left-inverse-of A₁≈A₂ x))
                  (to (B₁≈B₂ (from A₁≈A₂ (to A₁≈A₂ x)))
                      (f (from A₁≈A₂ (to A₁≈A₂ x)))))             ≡⟨ sym $ push-subst B₂  x y  from (B₁≈B₂ x) y)
                                                                                      (left-inverse-of A₁≈A₂ x) 
      subst B₁ (left-inverse-of A₁≈A₂ x)
            (from (B₁≈B₂ (from A₁≈A₂ (to A₁≈A₂ x)))
                  (to (B₁≈B₂ (from A₁≈A₂ (to A₁≈A₂ x)))
                      (f (from A₁≈A₂ (to A₁≈A₂ x)))))             ≡⟨ cong (subst B₁ (left-inverse-of A₁≈A₂ x)) $
                                                                       left-inverse-of (B₁≈B₂ _) _ 
      subst B₁ (left-inverse-of A₁≈A₂ x)
            (f (from A₁≈A₂ (to A₁≈A₂ x)))                         ≡⟨ elim  {x y} x≡y  subst B₁ x≡y (f x)  f y)
                                                                           x  subst-refl B₁ (f x))
                                                                          (left-inverse-of A₁≈A₂ x) ⟩∎
      f x                                                         

-- Weak equivalence preserves weak equivalences (assuming
-- extensionality).

≈-preserves :
   {a₁ a₂ b₁ b₂} 
  ({A : Set (a₁  a₂  b₁  b₂)} {B : A  Set (a₁  a₂  b₁  b₂)} 
   Extensionality A B) 
  {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : Set b₁} {B₂ : Set b₂} 
  A₁  A₂  B₁  B₂  (A₁  B₁)  (A₂  B₂)
≈-preserves {a₁} {a₂} {b₁} {b₂} ext {A₁} {A₂} {B₁} {B₂} A₁≈A₂ B₁≈B₂ =
  bijection⇒weak-equivalence (record
    { surjection = record
      { equivalence = record
        { to   = λ A₁≈B₁  B₁≈B₂  A₁≈B₁  inverse A₁≈A₂
        ; from = λ A₂≈B₂  inverse B₁≈B₂  A₂≈B₂  A₁≈A₂
        }
      ; right-inverse-of = to∘from
      }
    ; left-inverse-of = from∘to
    })
  where
  open _≈_

  abstract
    to∘from :
      (A₂≈B₂ : A₂  B₂) 
      B₁≈B₂  (inverse B₁≈B₂  A₂≈B₂  A₁≈A₂)  inverse A₁≈A₂  A₂≈B₂
    to∘from A₂≈B₂ =
      lift-equality (lower-extensionality (a₁  b₁) (a₁  b₁) ext) λ x 
          to B₁≈B₂ (from B₁≈B₂ (to A₂≈B₂ (to A₁≈A₂ (from A₁≈A₂ x))))  ≡⟨ right-inverse-of B₁≈B₂ _ 
          to A₂≈B₂ (to A₁≈A₂ (from A₁≈A₂ x))                          ≡⟨ cong (to A₂≈B₂) $ right-inverse-of A₁≈A₂ _ ⟩∎
          to A₂≈B₂ x                                                  

    from∘to :
      (A₁≈B₁ : A₁  B₁) 
      inverse B₁≈B₂  (B₁≈B₂  A₁≈B₁  inverse A₁≈A₂)  A₁≈A₂  A₁≈B₁
    from∘to A₁≈B₁ =
      lift-equality (lower-extensionality (a₂  b₂) (a₂  b₂) ext) λ x 
          from B₁≈B₂ (to B₁≈B₂ (to A₁≈B₁ (from A₁≈A₂ (to A₁≈A₂ x))))  ≡⟨ left-inverse-of B₁≈B₂ _ 
          to A₁≈B₁ (from A₁≈A₂ (to A₁≈A₂ x))                          ≡⟨ cong (to A₁≈B₁) $ left-inverse-of A₁≈A₂ _ ⟩∎
          to A₁≈B₁ x                                                  

-- Weak equivalence preserves bijections (assuming extensionality).

≈-preserves-bijections :
   {a₁ a₂ b₁ b₂} 
  ({A : Set (a₁  a₂  b₁  b₂)} {B : A  Set (a₁  a₂  b₁  b₂)} 
   Extensionality A B) 
  {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : Set b₁} {B₂ : Set b₂} 
  A₁  A₂  B₁  B₂  (A₁  B₁)  (A₂  B₂)
≈-preserves-bijections ext A₁↔A₂ B₁↔B₂ =
  _≈_.bijection $
    ≈-preserves ext (bijection⇒weak-equivalence A₁↔A₂)
                    (bijection⇒weak-equivalence B₁↔B₂)