------------------------------------------------------------------------
-- A universe which includes several kinds of functions
------------------------------------------------------------------------

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

open import Equality

module Function-universe
  {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open import Bijection eq as Bijection using (_↔_; module _↔_)
open Derived-definitions-and-properties eq
open import Embedding eq as Emb using (Is-embedding; Embedding)
open import Equality.Decidable-UIP eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq using (_≃_; module _≃_)
open import H-level eq as H-level
open import H-level.Closure eq
open import Injection eq as Injection using (_↣_; module _↣_; Injective)
open import Logical-equivalence using (_⇔_; module _⇔_)
open import Nat eq hiding (_≟_)
open import Preimage eq using (_⁻¹_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)
open import Surjection eq as Surjection using (_↠_; module _↠_)

------------------------------------------------------------------------
-- The universe

-- The universe includes implications, logical equivalences,
-- injections, embeddings, surjections, bijections and equivalences.

data Kind : Set where
  implication
    logical-equivalence
    injection
    embedding
    surjection
    bijection
    equivalence : Kind

-- The interpretation of the universe.

infix 0 _↝[_]_

_↝[_]_ :  {ℓ₁ ℓ₂}  Set ℓ₁  Kind  Set ℓ₂  Set _
A ↝[ implication         ] B = A  B
A ↝[ logical-equivalence ] B = A  B
A ↝[ injection           ] B = A  B
A ↝[ embedding           ] B = Embedding A B
A ↝[ surjection          ] B = A  B
A ↝[ bijection           ] B = A  B
A ↝[ equivalence         ] B = A  B

-- Equivalences can be converted to all kinds of functions.

from-equivalence :  {k a b} {A : Set a} {B : Set b} 
                   A  B  A ↝[ k ] B
from-equivalence {implication}         = _≃_.to
from-equivalence {logical-equivalence} = _≃_.logical-equivalence
from-equivalence {injection}           = _≃_.injection
from-equivalence {embedding}           = λ f  record
                                           { to           = _≃_.to f
                                           ; is-embedding = λ _ _ 
                                               _≃_.is-equivalence
                                                 (Eq.inverse (Eq.≃-≡ f))
                                           }
from-equivalence {surjection}          = _≃_.surjection
from-equivalence {bijection}           = _≃_.bijection
from-equivalence {equivalence}         = P.id

-- Bijections can be converted to all kinds of functions.

from-bijection :  {k a b} {A : Set a} {B : Set b} 
                 A  B  A ↝[ k ] B
from-bijection {implication}         = _↔_.to
from-bijection {logical-equivalence} = _↔_.logical-equivalence
from-bijection {injection}           = _↔_.injection
from-bijection {embedding}           = from-equivalence  Eq.↔⇒≃
from-bijection {surjection}          = _↔_.surjection
from-bijection {bijection}           = P.id
from-bijection {equivalence}         = Eq.↔⇒≃

-- All kinds of functions can be converted to implications.

to-implication :  {k a b} {A : Set a} {B : Set b} 
                 A ↝[ k ] B  A  B
to-implication {implication}         = P.id
to-implication {logical-equivalence} = _⇔_.to
to-implication {injection}           = _↣_.to
to-implication {embedding}           = Embedding.to
to-implication {surjection}          = _↠_.to
to-implication {bijection}           = _↔_.to
to-implication {equivalence}         = _≃_.to

------------------------------------------------------------------------
-- A sub-universe of symmetric kinds of functions

data Symmetric-kind : Set where
  logical-equivalence bijection equivalence : Symmetric-kind

⌊_⌋-sym : Symmetric-kind  Kind
 logical-equivalence ⌋-sym = logical-equivalence
 bijection           ⌋-sym = bijection
 equivalence         ⌋-sym = equivalence

inverse :  {k a b} {A : Set a} {B : Set b} 
          A ↝[  k ⌋-sym ] B  B ↝[  k ⌋-sym ] A
inverse {logical-equivalence} = Logical-equivalence.inverse
inverse {bijection}           = Bijection.inverse
inverse {equivalence}         = Eq.inverse

------------------------------------------------------------------------
-- A sub-universe of isomorphisms

data Isomorphism-kind : Set where
  bijection equivalence : Isomorphism-kind

⌊_⌋-iso : Isomorphism-kind  Kind
 bijection   ⌋-iso = bijection
 equivalence ⌋-iso = equivalence

infix 0 _↔[_]_

_↔[_]_ :  {ℓ₁ ℓ₂}  Set ℓ₁  Isomorphism-kind  Set ℓ₂  Set _
A ↔[ k ] B = A ↝[  k ⌋-iso ] B

from-isomorphism :  {k₁ k₂ a b} {A : Set a} {B : Set b} 
                   A ↔[ k₁ ] B  A ↝[ k₂ ] B
from-isomorphism {bijection}   = from-bijection
from-isomorphism {equivalence} = from-equivalence

-- Lemma: to-implication after from-isomorphism is the same as
-- to-implication.

to-implication∘from-isomorphism :
   {a b} {A : Set a} {B : Set b} k₁ k₂ {A↔B : A ↔[ k₁ ] B} 
  to-implication A↔B 
  to-implication (from-isomorphism {k₂ = k₂} A↔B)
to-implication∘from-isomorphism {A = A} {B} = t∘f
  where
  t∘f :  k₁ k₂ {A↔B : A ↔[ k₁ ] B} 
        to-implication A↔B 
        to-implication (from-isomorphism {k₂ = k₂} A↔B)
  t∘f bijection   implication         = refl _
  t∘f bijection   logical-equivalence = refl _
  t∘f bijection   injection           = refl _
  t∘f bijection   embedding           = refl _
  t∘f bijection   surjection          = refl _
  t∘f bijection   bijection           = refl _
  t∘f bijection   equivalence         = refl _
  t∘f equivalence implication         = refl _
  t∘f equivalence logical-equivalence = refl _
  t∘f equivalence injection           = refl _
  t∘f equivalence embedding           = refl _
  t∘f equivalence surjection          = refl _
  t∘f equivalence bijection           = refl _
  t∘f equivalence equivalence         = refl _

------------------------------------------------------------------------
-- Preorder

-- All the different kinds of functions form preorders.

-- Composition.

infixr 9 _∘_

_∘_ :  {k a b c} {A : Set a} {B : Set b} {C : Set c} 
      B ↝[ k ] C  A ↝[ k ] B  A ↝[ k ] C
_∘_ {implication}         = λ f g  f  g
_∘_ {logical-equivalence} = Logical-equivalence._∘_
_∘_ {injection}           = Injection._∘_
_∘_ {embedding}           = Emb._∘_
_∘_ {surjection}          = Surjection._∘_
_∘_ {bijection}           = Bijection._∘_
_∘_ {equivalence}         = Eq._∘_

-- Identity.

id :  {k a} {A : Set a}  A ↝[ k ] A
id {implication}         = P.id
id {logical-equivalence} = Logical-equivalence.id
id {injection}           = Injection.id
id {embedding}           = Emb.id
id {surjection}          = Surjection.id
id {bijection}           = Bijection.id
id {equivalence}         = Eq.id

-- "Equational" reasoning combinators.

infix  -1 finally-↝ finally-↔
infix  -1 _□
infixr -2 step-↝ step-↔ _↔⟨⟩_
infix  -3 $⟨_⟩_

-- For an explanation of why step-↝ and step-↔ are defined in this
-- way, see Equality.step-≡.

step-↝ :  {k a b c} (A : Set a) {B : Set b} {C : Set c} 
         B ↝[ k ] C  A ↝[ k ] B  A ↝[ k ] C
step-↝ _ = _∘_

syntax step-↝ A B↝C A↝B = A ↝⟨ A↝B ⟩ B↝C

step-↔ :  {k₁ k₂ a b c} (A : Set a) {B : Set b} {C : Set c} 
         B ↝[ k₂ ] C  A ↔[ k₁ ] B  A ↝[ k₂ ] C
step-↔ _ B↝C A↔B = step-↝ _ B↝C (from-isomorphism A↔B)

syntax step-↔ A B↝C A↔B = A ↔⟨ A↔B ⟩ B↝C

_↔⟨⟩_ :  {k a b} (A : Set a) {B : Set b} 
        A ↝[ k ] B  A ↝[ k ] B
_ ↔⟨⟩ A↝B = A↝B

_□ :  {k a} (A : Set a)  A ↝[ k ] A
A  = id

finally-↝ :  {k a b} (A : Set a) (B : Set b) 
            A ↝[ k ] B  A ↝[ k ] B
finally-↝ _ _ A↝B = A↝B

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

finally-↔ :  {k₁ k₂ a b} (A : Set a) (B : Set b) 
            A ↔[ k₁ ] B  A ↝[ k₂ ] B
finally-↔ _ _ A↔B = from-isomorphism A↔B

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

$⟨_⟩_ :  {k a b} {A : Set a} {B : Set b} 
        A  A ↝[ k ] B  B
$⟨ a  A↝B = to-implication A↝B a

-- Lemma: to-implication maps id to the identity function.

to-implication-id :
   {a} {A : Set a} k 
  to-implication {k = k} id  id {A = A}
to-implication-id implication         = refl _
to-implication-id logical-equivalence = refl _
to-implication-id injection           = refl _
to-implication-id embedding           = refl _
to-implication-id surjection          = refl _
to-implication-id bijection           = refl _
to-implication-id equivalence         = refl _

-- Lemma: to-implication is homomorphic with respect to _∘_.

to-implication-∘ :
   {a b c} {A : Set a} {B : Set b} {C : Set c} 
  (k : Kind) {f : A ↝[ k ] B} {g : B ↝[ k ] C} 
  to-implication (g  f)  to-implication g  to-implication f
to-implication-∘ implication         = refl _
to-implication-∘ logical-equivalence = refl _
to-implication-∘ injection           = refl _
to-implication-∘ embedding           = refl _
to-implication-∘ surjection          = refl _
to-implication-∘ bijection           = refl _
to-implication-∘ equivalence         = refl _

-- Lemma: to-implication maps inverse id to the identity function.

to-implication-inverse-id :
   {a} {A : Set a} k 
  to-implication (inverse {k = k} id)  id {A = A}
to-implication-inverse-id logical-equivalence = refl _
to-implication-inverse-id bijection           = refl _
to-implication-inverse-id equivalence         = refl _

------------------------------------------------------------------------
-- Conditional extensionality

-- Code that provides support for proving general statements about
-- functions of different kinds, in which the statements involve
-- assumptions of extensionality for some kinds of functions, but not
-- all. For some examples, see ∀-cong and ∀-intro.

-- Kinds for which extensionality is not provided.

data Without-extensionality : Set where
  implication logical-equivalence : Without-extensionality

⌊_⌋-without : Without-extensionality  Kind
 implication         ⌋-without = implication
 logical-equivalence ⌋-without = logical-equivalence

-- Kinds for which extensionality is provided.

data With-extensionality : Set where
  injection embedding surjection bijection equivalence :
    With-extensionality

⌊_⌋-with : With-extensionality  Kind
 injection   ⌋-with = injection
 embedding   ⌋-with = embedding
 surjection  ⌋-with = surjection
 bijection   ⌋-with = bijection
 equivalence ⌋-with = equivalence

-- Kinds annotated with information about whether extensionality is
-- provided or not.

data Extensionality-kind : Kind  Set where
  without-extensionality : (k : Without-extensionality) 
                           Extensionality-kind  k ⌋-without
  with-extensionality    : (k : With-extensionality) 
                           Extensionality-kind  k ⌋-with

-- Is extensionality provided for the given kind?

extensionality? : (k : Kind)  Extensionality-kind k
extensionality? implication         = without-extensionality implication
extensionality? logical-equivalence = without-extensionality
                                        logical-equivalence
extensionality? injection           = with-extensionality injection
extensionality? embedding           = with-extensionality embedding
extensionality? surjection          = with-extensionality surjection
extensionality? bijection           = with-extensionality bijection
extensionality? equivalence         = with-extensionality equivalence

-- Extensionality, but only for certain kinds of functions.

Extensionality? : Kind  (a b : Level)  Set (lsuc (a  b))
Extensionality? k with extensionality? k
... | without-extensionality _ = λ _ _   _ 
... | with-extensionality    _ = Extensionality

-- Turns extensionality into conditional extensionality.

forget-ext? :  k {a b}  Extensionality a b  Extensionality? k a b
forget-ext? k with extensionality? k
... | without-extensionality _ = _
... | with-extensionality    _ = id

-- A variant of lower-extensionality.

lower-extensionality? :
   k {a}  {b}  
  Extensionality? k (a  ) (b  )  Extensionality? k a b
lower-extensionality? k with extensionality? k
... | without-extensionality _ = _
... | with-extensionality    _ = lower-extensionality

-- A function that can be used to generalise results.

generalise-ext? :
   {a b c d} {A : Set a} {B : Set b} 
  A  B 
  (Extensionality c d  A  B) 
   {k}  Extensionality? k c d  A ↝[ k ] B
generalise-ext? f⇔ f↔ {k} with extensionality? k
... | without-extensionality implication         = λ _  _⇔_.to f⇔
... | without-extensionality logical-equivalence = λ _  f⇔
... | with-extensionality    _                   = λ ext 
  from-isomorphism (f↔ ext)

-- General results of the kind produced by generalise-ext? are
-- symmetric.

inverse-ext? :
   {a b c d} {A : Set a} {B : Set b} 
  (∀ {k}  Extensionality? k c d  A ↝[ k ] B) 
  (∀ {k}  Extensionality? k c d  B ↝[ k ] A)
inverse-ext? hyp = generalise-ext? (inverse $ hyp _) (inverse  hyp)

------------------------------------------------------------------------
-- Lots of properties
------------------------------------------------------------------------

-- Properties of the form A ↝[ k ] B, for arbitrary k, are only stated
-- for bijections or equivalences; converting to the other forms is
-- easy.

------------------------------------------------------------------------
-- Equalities can be converted to all kinds of functions

≡⇒↝ :  k {} {A B : Set }  A  B  A ↝[ k ] B
≡⇒↝ k = elim  {A B} _  A ↝[ k ] B)  _  id)

abstract

  -- Some lemmas that can be used to manipulate expressions involving
  -- ≡⇒↝ and refl/sym/trans.

  ≡⇒↝-refl :  {k a} {A : Set a} 
             ≡⇒↝ k (refl A)  id
  ≡⇒↝-refl {k} = elim-refl  {A B} _  A ↝[ k ] B) _

  ≡⇒↝-sym :  k {} {A B : Set } {eq : A  B} 
            to-implication (≡⇒↝  k ⌋-sym (sym eq)) 
            to-implication (inverse (≡⇒↝  k ⌋-sym eq))
  ≡⇒↝-sym k {A = A} {eq = eq} = elim¹
     eq  to-implication (≡⇒↝  k ⌋-sym (sym eq)) 
            to-implication (inverse (≡⇒↝  k ⌋-sym eq)))
    (to-implication (≡⇒↝  k ⌋-sym (sym (refl A)))      ≡⟨ cong (to-implication  ≡⇒↝  k ⌋-sym) sym-refl 
     to-implication (≡⇒↝  k ⌋-sym (refl A))            ≡⟨ cong (to-implication {k =  k ⌋-sym}) ≡⇒↝-refl 
     to-implication {k =  k ⌋-sym} id                  ≡⟨ to-implication-id  k ⌋-sym 
     id                                                 ≡⟨ sym $ to-implication-inverse-id k 
     to-implication (inverse {k = k} id)                ≡⟨ cong (to-implication  inverse {k = k}) $ sym ≡⇒↝-refl ⟩∎
     to-implication (inverse (≡⇒↝  k ⌋-sym (refl A)))  )
    eq

  ≡⇒↝-trans :  k {} {A B C : Set } {A≡B : A  B} {B≡C : B  C} 
              to-implication (≡⇒↝ k (trans A≡B B≡C)) 
              to-implication (≡⇒↝ k B≡C  ≡⇒↝ k A≡B)
  ≡⇒↝-trans k {B = B} {A≡B = A≡B} = elim¹
     B≡C  to-implication (≡⇒↝ k (trans A≡B B≡C)) 
             to-implication (≡⇒↝ k B≡C  ≡⇒↝ k A≡B))
    (to-implication (≡⇒↝ k (trans A≡B (refl B)))             ≡⟨ cong (to-implication  ≡⇒↝ k) $ trans-reflʳ _ 
     to-implication (≡⇒↝ k A≡B)                              ≡⟨ sym $ cong  f  f  to-implication (≡⇒↝ k A≡B)) $ to-implication-id k 
     to-implication {k = k} id  to-implication (≡⇒↝ k A≡B)  ≡⟨ sym $ to-implication-∘ k 
     to-implication (id  ≡⇒↝ k A≡B)                         ≡⟨ sym $ cong  f  to-implication (f  ≡⇒↝ k A≡B)) ≡⇒↝-refl ⟩∎
     to-implication (≡⇒↝ k (refl B)  ≡⇒↝ k A≡B)             )
    _

  -- One can sometimes "push" ≡⇒↝ through cong.
  --
  -- This is a generalisation of a lemma due to Thierry Coquand.

  ≡⇒↝-cong :  {k  p A B} {eq : A  B}
             (P : Set   Set p)
             (P-cong :  {A B}  A ↝[ k ] B  P A ↝[ k ] P B) 
             P-cong (id {A = A})  id 
             ≡⇒↝ _ (cong P eq)  P-cong (≡⇒↝ _ eq)
  ≡⇒↝-cong {eq = eq} P P-cong P-cong-id = elim¹
     eq  ≡⇒↝ _ (cong P eq)  P-cong (≡⇒↝ _ eq))
    (≡⇒↝ _ (cong P (refl _))  ≡⟨ cong (≡⇒↝ _) $ cong-refl P 
     ≡⇒↝ _ (refl _)           ≡⟨ elim-refl  {A B} _  A ↝[ _ ] B) _ 
     id                       ≡⟨ sym P-cong-id 
     P-cong id                ≡⟨ cong P-cong $ sym $
                                   elim-refl  {A B} _  A ↝[ _ ] B) _ ⟩∎
     P-cong (≡⇒↝ _ (refl _))  )
    eq

  -- One can express subst in terms of ≡⇒↝.

  subst-in-terms-of-≡⇒↝ :
     k {a p} {A : Set a} {x y} (x≡y : x  y) (P : A  Set p) p 
    subst P x≡y p  to-implication (≡⇒↝ k (cong P x≡y)) p
  subst-in-terms-of-≡⇒↝ k x≡y P p = elim¹

     eq  subst P eq p  to-implication (≡⇒↝ k (cong P eq)) p)

    (subst P (refl _) p                          ≡⟨ subst-refl P p 
     p                                           ≡⟨ sym $ cong (_$ p) (to-implication-id k) 
     to-implication {k = k} id p                 ≡⟨ sym $ cong  f  to-implication {k = k} f p) ≡⇒↝-refl 
     to-implication (≡⇒↝ k (refl _)) p           ≡⟨ sym $ cong  eq  to-implication (≡⇒↝ k eq) p) $ cong-refl P ⟩∎
     to-implication (≡⇒↝ k (cong P (refl _))) p  )

    x≡y

  subst-in-terms-of-inverse∘≡⇒↝ :
     k {a p} {A : Set a} {x y} (x≡y : x  y) (P : A  Set p) p 
    subst P (sym x≡y) p 
    to-implication (inverse (≡⇒↝  k ⌋-sym (cong P x≡y))) p
  subst-in-terms-of-inverse∘≡⇒↝ k x≡y P p =
    subst P (sym x≡y) p                                      ≡⟨ subst-in-terms-of-≡⇒↝  k ⌋-sym (sym x≡y) P p 
    to-implication (≡⇒↝  k ⌋-sym (cong P (sym x≡y))) p      ≡⟨ cong  eq  to-implication (≡⇒↝  k ⌋-sym eq) p) (cong-sym P _) 
    to-implication (≡⇒↝  k ⌋-sym (sym $ cong P x≡y)) p      ≡⟨ cong (_$ p) (≡⇒↝-sym k) ⟩∎
    to-implication (inverse (≡⇒↝  k ⌋-sym (cong P x≡y))) p  

  to-implication-≡⇒↝ :
     k {} {A B : Set } (eq : A  B) 
    to-implication (≡⇒↝ k eq)  ≡⇒↝ implication eq
  to-implication-≡⇒↝ k =
    elim  eq  to-implication (≡⇒↝ k eq)  ≡⇒↝ implication eq)
          A  to-implication (≡⇒↝ k (refl A))  ≡⟨ cong to-implication (≡⇒↝-refl {k = k}) 
                to-implication {k = k} id        ≡⟨ to-implication-id k 
                id                               ≡⟨ sym ≡⇒↝-refl ⟩∎
                ≡⇒↝ implication (refl A)         )

------------------------------------------------------------------------
-- _⊎_ is a commutative monoid

-- _⊎_ preserves all kinds of functions.

private

  ⊎-cong-eq :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                {B₁ : Set b₁} {B₂ : Set b₂} 
              A₁  A₂  B₁  B₂  A₁  B₁  A₂  B₂
  ⊎-cong-eq A₁⇔A₂ B₁⇔B₂ = record
    { to   = ⊎-map (to   A₁⇔A₂) (to   B₁⇔B₂)
    ; from = ⊎-map (from A₁⇔A₂) (from B₁⇔B₂)
    } where open _⇔_

  ⊎-cong-inj :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                 {B₁ : Set b₁} {B₂ : Set b₂} 
               A₁  A₂  B₁  B₂  A₁  B₁  A₂  B₂
  ⊎-cong-inj A₁↣A₂ B₁↣B₂ = record
    { to        = to′
    ; injective = injective′
    }
    where
    open _↣_

    to′ = ⊎-map (to A₁↣A₂) (to B₁↣B₂)

    abstract
      injective′ : Injective to′
      injective′ {x = inj₁ x} {y = inj₁ y} = cong inj₁  injective A₁↣A₂  ⊎.cancel-inj₁
      injective′ {x = inj₂ x} {y = inj₂ y} = cong inj₂  injective B₁↣B₂  ⊎.cancel-inj₂
      injective′ {x = inj₁ x} {y = inj₂ y} = ⊥-elim  ⊎.inj₁≢inj₂
      injective′ {x = inj₂ x} {y = inj₁ y} = ⊥-elim  ⊎.inj₁≢inj₂  sym

  ⊎-cong-emb :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                 {B₁ : Set b₁} {B₂ : Set b₂} 
               Embedding A₁ A₂  Embedding B₁ B₂ 
               Embedding (A₁  B₁) (A₂  B₂)
  ⊎-cong-emb A₁↣A₂ B₁↣B₂ = record
    { to           = to′
    ; is-embedding = is-embedding′
    }
    where
    open Embedding

    to′ = ⊎-map (to A₁↣A₂) (to B₁↣B₂)

    is-embedding′ : Is-embedding to′
    is-embedding′ (inj₁ x) (inj₁ y) =
      _≃_.is-equivalence $
      Eq.with-other-function
        (inj₁ x  inj₁ y                        ↔⟨ inverse Bijection.≡↔inj₁≡inj₁ 
         x  y                                  ↝⟨ Eq.⟨ _ , is-embedding A₁↣A₂ _ _  
         to A₁↣A₂ x  to A₁↣A₂ y                ↔⟨ Bijection.≡↔inj₁≡inj₁ ⟩□
         inj₁ (to A₁↣A₂ x)  inj₁ (to A₁↣A₂ y)  )
        _
         eq 
           cong inj₁ (cong (to A₁↣A₂) (⊎.cancel-inj₁ eq))                 ≡⟨ cong-∘ _ _ _ 
           cong (inj₁  to A₁↣A₂) (⊎.cancel-inj₁ eq)                      ≡⟨ cong-∘ _ _ _ 
           cong (inj₁  to A₁↣A₂  [ id , const x ]) eq                   ≡⟨ sym $ trans-reflʳ _ 
           trans (cong (inj₁  to A₁↣A₂  [ id , const x ]) eq) (refl _)  ≡⟨ cong-respects-relevant-equality
                                                                               {f = inj₁  to A₁↣A₂  [ id , const x ]}
                                                                               (if_then true else false)
                                                                               [  _ _  refl _) ,  _ ()) ] 
           trans (refl _) (cong (⊎-map (to A₁↣A₂) (to B₁↣B₂)) eq)         ≡⟨ trans-reflˡ _ ⟩∎
           cong (⊎-map (to A₁↣A₂) (to B₁↣B₂)) eq                          )

    is-embedding′ (inj₂ x) (inj₂ y) =
      _≃_.is-equivalence $
      Eq.with-other-function
        (inj₂ x  inj₂ y                        ↔⟨ inverse Bijection.≡↔inj₂≡inj₂ 
         x  y                                  ↝⟨ Eq.⟨ _ , is-embedding B₁↣B₂ _ _  
         to B₁↣B₂ x  to B₁↣B₂ y                ↔⟨ Bijection.≡↔inj₂≡inj₂ ⟩□
         inj₂ (to B₁↣B₂ x)  inj₂ (to B₁↣B₂ y)  )
        _
         eq 
           cong inj₂ (cong (to B₁↣B₂) (⊎.cancel-inj₂ eq))                 ≡⟨ cong-∘ _ _ _ 
           cong (inj₂  to B₁↣B₂) (⊎.cancel-inj₂ eq)                      ≡⟨ cong-∘ _ _ _ 
           cong (inj₂  to B₁↣B₂  [ const x , id ]) eq                   ≡⟨ sym $ trans-reflʳ _ 
           trans (cong (inj₂  to B₁↣B₂  [ const x , id ]) eq) (refl _)  ≡⟨ cong-respects-relevant-equality
                                                                               {f = inj₂  to B₁↣B₂  [ const x , id ]}
                                                                               (if_then false else true)
                                                                               [  _ ()) ,  _ _  refl _) ] 
           trans (refl _) (cong (⊎-map (to A₁↣A₂) (to B₁↣B₂)) eq)         ≡⟨ trans-reflˡ _ ⟩∎
           cong (⊎-map (to A₁↣A₂) (to B₁↣B₂)) eq                          )

    is-embedding′ (inj₁ x) (inj₂ y) =
      _≃_.is-equivalence $
      Eq.with-other-function
        (inj₁ x  inj₂ y                        ↔⟨ inverse $ Bijection.⊥↔uninhabited ⊎.inj₁≢inj₂ 
         ⊥₀                                     ↔⟨ Bijection.⊥↔uninhabited ⊎.inj₁≢inj₂ ⟩□
         inj₁ (to A₁↣A₂ x)  inj₂ (to B₁↣B₂ y)  )
        _
        (⊥-elim  ⊎.inj₁≢inj₂)

    is-embedding′ (inj₂ x) (inj₁ y) =
      _≃_.is-equivalence $
      Eq.with-other-function
        (inj₂ x  inj₁ y                        ↔⟨ inverse $ Bijection.⊥↔uninhabited (⊎.inj₁≢inj₂  sym) 
         ⊥₀                                     ↔⟨ Bijection.⊥↔uninhabited (⊎.inj₁≢inj₂  sym) ⟩□
         inj₂ (to B₁↣B₂ x)  inj₁ (to A₁↣A₂ y)  )
        _
        (⊥-elim  ⊎.inj₁≢inj₂  sym)

  ⊎-cong-surj :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                  {B₁ : Set b₁} {B₂ : Set b₂} 
                A₁  A₂  B₁  B₂  A₁  B₁  A₂  B₂
  ⊎-cong-surj A₁↠A₂ B₁↠B₂ = record
    { logical-equivalence = ⊎-cong-eq (_↠_.logical-equivalence A₁↠A₂)
                                      (_↠_.logical-equivalence B₁↠B₂)
    ; right-inverse-of    =
        [ cong inj₁  _↠_.right-inverse-of A₁↠A₂
        , cong inj₂  _↠_.right-inverse-of B₁↠B₂
        ]
    }

  ⊎-cong-bij :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                 {B₁ : Set b₁} {B₂ : Set b₂} 
               A₁  A₂  B₁  B₂  A₁  B₁  A₂  B₂
  ⊎-cong-bij A₁↔A₂ B₁↔B₂ = record
    { surjection      = ⊎-cong-surj (_↔_.surjection A₁↔A₂)
                                    (_↔_.surjection B₁↔B₂)
    ; left-inverse-of =
        [ cong inj₁  _↔_.left-inverse-of A₁↔A₂
        , cong inj₂  _↔_.left-inverse-of B₁↔B₂
        ]
    }

infixr 1 _⊎-cong_

_⊎-cong_ :  {k a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
             {B₁ : Set b₁} {B₂ : Set b₂} 
           A₁ ↝[ k ] A₂  B₁ ↝[ k ] B₂  A₁  B₁ ↝[ k ] A₂  B₂
_⊎-cong_ {implication}         = ⊎-map
_⊎-cong_ {logical-equivalence} = ⊎-cong-eq
_⊎-cong_ {injection}           = ⊎-cong-inj
_⊎-cong_ {embedding}           = ⊎-cong-emb
_⊎-cong_ {surjection}          = ⊎-cong-surj
_⊎-cong_ {bijection}           = ⊎-cong-bij
_⊎-cong_ {equivalence}         = λ A₁≃A₂ B₁≃B₂ 
  from-bijection $ ⊎-cong-bij (from-equivalence A₁≃A₂)
                              (from-equivalence B₁≃B₂)

-- _⊎_ is commutative.

⊎-comm :  {a b} {A : Set a} {B : Set b}  A  B  B  A
⊎-comm = record
  { surjection = record
    { logical-equivalence = record
      { to   = [ inj₂ , inj₁ ]
      ; from = [ inj₂ , inj₁ ]
      }
    ; right-inverse-of = [ refl  inj₁ , refl  inj₂ ]
    }
  ; left-inverse-of = [ refl  inj₁ , refl  inj₂ ]
  }

-- _⊎_ is associative.

⊎-assoc :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
          A  (B  C)  (A  B)  C
⊎-assoc = record
  { surjection = record
    { logical-equivalence = record
      { to   = [ inj₁  inj₁ , [ inj₁  inj₂ , inj₂ ] ]
      ; from = [ [ inj₁ , inj₂  inj₁ ] , inj₂  inj₂ ]
      }
    ; right-inverse-of =
        [ [ refl  inj₁  inj₁ , refl  inj₁  inj₂ ] , refl  inj₂ ]
    }
  ; left-inverse-of =
      [ refl  inj₁ , [ refl  inj₂  inj₁ , refl  inj₂  inj₂ ] ]
  }

-- ⊥ is a left and right identity of _⊎_.

⊎-left-identity :  {a } {A : Set a}   { = }  A  A
⊎-left-identity = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (inj₁ ()); (inj₂ x)  x }
      ; from = inj₂
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = λ { (inj₁ ()); (inj₂ x)  refl (inj₂ x) }
  }

⊎-right-identity :  {a } {A : Set a}  A   { = }  A
⊎-right-identity {A = A} =
  A    ↔⟨ ⊎-comm 
    A  ↔⟨ ⊎-left-identity ⟩□
  A      

-- For logical equivalences _⊎_ is also idempotent. (This lemma could
-- be generalised to cover surjections and implications.)

⊎-idempotent :  {a} {A : Set a}  A  A  A
⊎-idempotent = record
  { to   = [ id , id ]
  ; from = inj₁
  }

------------------------------------------------------------------------
-- _×_ is a commutative monoid with a zero

-- Σ preserves embeddings. (This definition is used in the proof of
-- _×-cong_.)

Σ-preserves-embeddings :
   {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂}
  (A₁↣A₂ : Embedding A₁ A₂) 
  (∀ x  Embedding (B₁ x) (B₂ (Embedding.to A₁↣A₂ x))) 
  Embedding (Σ A₁ B₁) (Σ A₂ B₂)
Σ-preserves-embeddings {B₁ = B₁} {B₂} A₁↣A₂ B₁↣B₂ = record
  { to           = Σ-map (to A₁↣A₂) (to (B₁↣B₂ _))
  ; is-embedding = λ { (x₁ , x₂) (y₁ , y₂) 
      _≃_.is-equivalence $
      Eq.with-other-function
        ((x₁ , x₂)  (y₁ , y₂)                                   ↝⟨ inverse $ Eq.↔⇒≃ Bijection.Σ-≡,≡↔≡ 

         ( λ (eq : x₁  y₁)  subst B₁ eq x₂  y₂)              ↝⟨ Eq.Σ-preserves (Embedding.equivalence A₁↣A₂)  eq 

             subst B₁ eq x₂  y₂                                      ↝⟨ Embedding.equivalence (B₁↣B₂ y₁) 

             to (B₁↣B₂ y₁) (subst B₁ eq x₂)  to (B₁↣B₂ y₁) y₂        ↝⟨ ≡⇒↝ _ (cong (_≡ _) $ lemma₁ eq _ y₂) ⟩□

             subst B₂ (cong (to A₁↣A₂) eq) (to (B₁↣B₂ x₁) x₂) 
             to (B₁↣B₂ y₁) y₂                                         ) 

         ( λ (eq : to A₁↣A₂ x₁  to A₁↣A₂ y₁) 
            subst B₂ eq (to (B₁↣B₂ x₁) x₂)  to (B₁↣B₂ y₁) y₂)   ↝⟨ Eq.↔⇒≃ Bijection.Σ-≡,≡↔≡ ⟩□

         (to A₁↣A₂ x₁ , to (B₁↣B₂ x₁) x₂) 
         (to A₁↣A₂ y₁ , to (B₁↣B₂ y₁) y₂)                        )
        _
        (elim
           { {y = _ , y₂} eq 
               uncurry Σ-≡,≡→≡
                 (Σ-map (cong (to A₁↣A₂))
                        (_≃_.to (≡⇒↝ _ (cong (_≡ _) $ lemma₁ _ _ y₂)) 
                         cong (to (B₁↣B₂ _)))
                        (Σ-≡,≡←≡ eq)) 
               cong (Σ-map (to A₁↣A₂) (to (B₁↣B₂ _))) eq })
           _ 
             uncurry Σ-≡,≡→≡
               (Σ-map (cong (to A₁↣A₂))
                      (_≃_.to (≡⇒↝ _ (cong (_≡ _) $ lemma₁ _ _ _)) 
                       cong (to (B₁↣B₂ _)))
                      (Σ-≡,≡←≡ (refl _)))                                 ≡⟨ cong  eq  uncurry Σ-≡,≡→≡
                                                                                            (Σ-map _
                                                                                                   (_≃_.to (≡⇒↝ _ (cong (_≡ _) $ lemma₁ _ _ _)) 
                                                                                                    cong (to (B₁↣B₂ _)))
                                                                                                   eq))
                                                                                  Σ-≡,≡←≡-refl 
             Σ-≡,≡→≡
               (cong (to A₁↣A₂) (refl _))
               (_≃_.to (≡⇒↝ _ (cong (_≡ to (B₁↣B₂ _) _) $ lemma₁ _ _ _))
                  (cong (to (B₁↣B₂ _)) (subst-refl B₁ _)))                ≡⟨ Σ-≡,≡→≡-cong (cong-refl _) (lemma₂ _ _) 

             Σ-≡,≡→≡ (refl _) (subst-refl B₂ _)                           ≡⟨ Σ-≡,≡→≡-refl-subst-refl 

             refl _                                                       ≡⟨ sym $ cong-refl _ ⟩∎

             cong (Σ-map (to A₁↣A₂) (to (B₁↣B₂ _))) (refl _)              )) }
  }
  where
  open Embedding using (to)

  lemma₁ = elim
     {x₁ y₁} eq  (x₂ : B₁ x₁) (y₂ : B₁ y₁) 
       to (B₁↣B₂ y₁) (subst B₁ eq x₂) 
       subst B₂ (cong (to A₁↣A₂) eq) (to (B₁↣B₂ x₁) x₂))
     z₁ x₂ y₂ 
       to (B₁↣B₂ z₁) (subst B₁ (refl z₁) x₂)                    ≡⟨ cong (to (B₁↣B₂ z₁)) $ subst-refl _ _ 
       to (B₁↣B₂ z₁) x₂                                         ≡⟨ sym $ subst-refl _ _ 
       subst B₂ (refl (to A₁↣A₂ z₁)) (to (B₁↣B₂ z₁) x₂)         ≡⟨ cong  eq  subst B₂ eq _) (sym $ cong-refl _) ⟩∎
       subst B₂ (cong (to A₁↣A₂) (refl z₁)) (to (B₁↣B₂ z₁) x₂)  )

  lemma₂ = λ x y 
    let eq₁ = cong (flip (subst B₂) _) (sym (cong-refl _))
        eq₂ = cong (to (B₁↣B₂ x)) (subst-refl B₁ y)
    in
    trans eq₁ (_≃_.to (≡⇒↝ _ (cong (_≡ _) $ lemma₁ (refl x) y y)) eq₂)   ≡⟨ cong  eq  trans eq₁ (_≃_.to (≡⇒↝ _ (cong (_≡ _) (eq y y))) eq₂)) $
                                                                              elim-refl  {x₁ y₁} eq  (x₂ : B₁ x₁) (y₂ : B₁ y₁) 
                                                                                           to (B₁↣B₂ y₁) (subst B₁ eq x₂) 
                                                                                           subst B₂ (cong (to A₁↣A₂) eq) (to (B₁↣B₂ x₁) x₂))
                                                                                        _ 
    trans eq₁ (_≃_.to (≡⇒↝ _ $ cong (_≡ _) $
                         trans eq₂ (trans (sym $ subst-refl B₂ _) eq₁))
                 eq₂)                                                    ≡⟨ cong (trans _) $ sym $ subst-in-terms-of-≡⇒↝ equivalence _ _ _ 

    trans eq₁ (subst (_≡ _)
                 (trans eq₂ (trans (sym $ subst-refl B₂ _) eq₁))
                 eq₂)                                                    ≡⟨ cong  eq  trans eq₁ (subst (_≡ _) eq eq₂)) $
                                                                              sym $ sym-sym (trans eq₂ (trans (sym $ subst-refl B₂ _) eq₁)) 
    trans eq₁ (subst (_≡ _)
                 (sym $ sym $
                    trans eq₂ (trans (sym $ subst-refl B₂ _) eq₁))
                 eq₂)                                                    ≡⟨ cong (trans _) $ subst-trans _ 

    trans eq₁ (trans
                 (sym $ trans eq₂ (trans (sym $ subst-refl B₂ _) eq₁))
                 eq₂)                                                    ≡⟨ cong  eq  trans eq₁ (trans eq eq₂)) $
                                                                              sym-trans eq₂ (trans (sym $ subst-refl B₂ _) eq₁) 
    trans eq₁ (trans (trans (sym $ trans (sym $ subst-refl B₂ _) eq₁)
                            (sym eq₂))
                     eq₂)                                                ≡⟨ cong (trans _) $ trans-[trans-sym]- _ _ 

    trans eq₁ (sym $ trans (sym $ subst-refl B₂ _) eq₁)                  ≡⟨ cong (trans _) $ sym-trans _ _ 

    trans eq₁ (trans (sym eq₁) (sym $ sym $ subst-refl B₂ _))            ≡⟨ trans--[trans-sym] _ _ 

    sym $ sym $ subst-refl B₂ _                                          ≡⟨ sym-sym _ ⟩∎

    subst-refl B₂ _                                                      

-- _×_ preserves all kinds of functions.

private

  ×-cong-eq :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                {B₁ : Set b₁} {B₂ : Set b₂} 
              A₁  A₂  B₁  B₂  A₁ × B₁  A₂ × B₂
  ×-cong-eq A₁⇔A₂ B₁⇔B₂ = record
    { to   = Σ-map (to   A₁⇔A₂) (to   B₁⇔B₂)
    ; from = Σ-map (from A₁⇔A₂) (from B₁⇔B₂)
    } where open _⇔_

  ×-cong-inj :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                 {B₁ : Set b₁} {B₂ : Set b₂} 
               A₁  A₂  B₁  B₂  A₁ × B₁  A₂ × B₂
  ×-cong-inj {A₁ = A₁} {A₂} {B₁} {B₂} A₁↣A₂ B₁↣B₂ = record
    { to        = to′
    ; injective = injective′
    }
    where
    open _↣_

    to′ : A₁ × B₁  A₂ × B₂
    to′ = Σ-map (to A₁↣A₂) (to B₁↣B₂)

    abstract
      injective′ : Injective to′
      injective′ to′-x≡to′-y =
        cong₂ _,_ (injective A₁↣A₂ (cong proj₁ to′-x≡to′-y))
                  (injective B₁↣B₂ (cong proj₂ to′-x≡to′-y))

  ×-cong-surj :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                  {B₁ : Set b₁} {B₂ : Set b₂} 
                A₁  A₂  B₁  B₂  A₁ × B₁  A₂ × B₂
  ×-cong-surj A₁↠A₂ B₁↠B₂ = record
    { logical-equivalence = ×-cong-eq (_↠_.logical-equivalence A₁↠A₂)
                                      (_↠_.logical-equivalence B₁↠B₂)
    ; right-inverse-of    = uncurry λ x y 
        cong₂ _,_ (_↠_.right-inverse-of A₁↠A₂ x)
                  (_↠_.right-inverse-of B₁↠B₂ y)
    }

  ×-cong-bij :  {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                 {B₁ : Set b₁} {B₂ : Set b₂} 
               A₁  A₂  B₁  B₂  A₁ × B₁  A₂ × B₂
  ×-cong-bij A₁↔A₂ B₁↔B₂ = record
    { surjection      = ×-cong-surj (_↔_.surjection A₁↔A₂)
                                    (_↔_.surjection B₁↔B₂)
    ; left-inverse-of = uncurry λ x y 
        cong₂ _,_ (_↔_.left-inverse-of A₁↔A₂ x)
                  (_↔_.left-inverse-of B₁↔B₂ y)
    }

infixr 2 _×-cong_

_×-cong_ :  {k a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
             {B₁ : Set b₁} {B₂ : Set b₂} 
           A₁ ↝[ k ] A₂  B₁ ↝[ k ] B₂  A₁ × B₁ ↝[ k ] A₂ × B₂
_×-cong_ {implication}         = λ f g  Σ-map f g
_×-cong_ {logical-equivalence} = ×-cong-eq
_×-cong_ {injection}           = ×-cong-inj
_×-cong_ {embedding}           = λ A₁↣A₂ B₁↣B₂ 
                                   Σ-preserves-embeddings
                                     A₁↣A₂  _  B₁↣B₂)
_×-cong_ {surjection}          = ×-cong-surj
_×-cong_ {bijection}           = ×-cong-bij
_×-cong_ {equivalence}         = λ A₁≃A₂ B₁≃B₂ 
  from-bijection $ ×-cong-bij (from-equivalence A₁≃A₂)
                              (from-equivalence B₁≃B₂)

-- _×_ is commutative.

×-comm :  {a b} {A : Set a} {B : Set b}  A × B  B × A
×-comm = record
  { surjection = record
    { logical-equivalence = record
      { to   = uncurry λ x y  (y , x)
      ; from = uncurry λ x y  (y , x)
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Σ is associative.

Σ-assoc :  {a b c}
            {A : Set a} {B : A  Set b} {C : (x : A)  B x  Set c} 
          (Σ A λ x  Σ (B x) (C x))  Σ (Σ A B) (uncurry C)
Σ-assoc = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (x , (y , z))  (x , y) , z }
      ; from = λ { ((x , y) , z)  x , (y , z) }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- _×_ is associative.

×-assoc :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
          A × (B × C)  (A × B) × C
×-assoc = Σ-assoc

-- ⊤ is a left and right identity of _×_ and Σ.

Σ-left-identity :  {a} {A :   Set a}  Σ  A  A tt
Σ-left-identity = record
  { surjection = record
    { logical-equivalence = record
      { to   = proj₂
      ; from = λ x  (tt , x)
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

×-left-identity :  {a} {A : Set a}   × A  A
×-left-identity = Σ-left-identity

×-right-identity :  {a} {A : Set a}  A ×   A
×-right-identity {A = A} =
  A ×   ↔⟨ ×-comm 
   × A  ↔⟨ ×-left-identity ⟩□
  A      

-- ⊥ is a left and right zero of _×_ and Σ.

Σ-left-zero :  {ℓ₁ a ℓ₂} {A :  { = ℓ₁}  Set a} 
              Σ  A   { = ℓ₂}
Σ-left-zero = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ { (() , _) }
      ; from = λ ()
      }
    ; right-inverse-of = λ ()
    }
  ; left-inverse-of = λ { (() , _) }
  }

×-left-zero :  {a ℓ₁ ℓ₂} {A : Set a}   { = ℓ₁} × A   { = ℓ₂}
×-left-zero = Σ-left-zero

×-right-zero :  {a ℓ₁ ℓ₂} {A : Set a}  A ×  { = ℓ₁}   { = ℓ₂}
×-right-zero {A = A} =
  A ×   ↔⟨ ×-comm 
   × A  ↔⟨ ×-left-zero ⟩□
        

------------------------------------------------------------------------
-- Some lemmas related to Σ/∃/_×_

-- See also Σ-left-zero and Σ-right-zero above.

-- Σ preserves isomorphisms in its first argument and all kinds of
-- functions in its second argument.
--
-- The first two clauses are included as an optimisation intended to
-- make some proof terms easier to work with.

Σ-cong :  {k₁ k₂ a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
           {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
         (A₁↔A₂ : A₁ ↔[ k₁ ] A₂) 
         (∀ x  B₁ x ↝[ k₂ ] B₂ (to-implication A₁↔A₂ x)) 
         Σ A₁ B₁ ↝[ k₂ ] Σ A₂ B₂
Σ-cong {equivalence} {equivalence} A₁≃A₂ B₁≃B₂ =
  Eq.Σ-preserves A₁≃A₂ B₁≃B₂
Σ-cong {equivalence} {bijection} A₁≃A₂ B₁↔B₂ =
  Eq.∃-preserves-bijections A₁≃A₂ B₁↔B₂
Σ-cong {k₁} {k₂} {A₁ = A₁} {A₂} {B₁} {B₂} A₁↔A₂ B₁↝B₂ = helper k₂ B₁↝B₂′
  where
  A₁≃A₂ : A₁  A₂
  A₁≃A₂ = from-isomorphism A₁↔A₂

  B₁↝B₂′ :  x  B₁ x ↝[ k₂ ] B₂ (_≃_.to A₁≃A₂ x)
  B₁↝B₂′ x =
    B₁ x                                    ↝⟨ B₁↝B₂ x 
    B₂ (to-implication A₁↔A₂ x)             ↝⟨ ≡⇒↝ _ $ cong  f  B₂ (f x)) $
                                                 to-implication∘from-isomorphism k₁ equivalence 
    B₂ (_≃_.to (from-isomorphism A₁↔A₂) x)  

  helper :  k₂  (∀ x  B₁ x ↝[ k₂ ] B₂ (_≃_.to A₁≃A₂ x)) 
           Σ A₁ B₁ ↝[ k₂ ] Σ A₂ B₂
  helper implication         = Eq.∃-preserves-functions            A₁≃A₂
  helper logical-equivalence = Eq.∃-preserves-logical-equivalences A₁≃A₂
  helper injection           = Eq.∃-preserves-injections           A₁≃A₂
  helper embedding           = Σ-preserves-embeddings
                                 (from-equivalence A₁≃A₂)
  helper surjection          = Eq.∃-preserves-surjections          A₁≃A₂
  helper bijection           = Eq.∃-preserves-bijections           A₁≃A₂
  helper equivalence         = Eq.Σ-preserves                      A₁≃A₂

-- ∃ preserves all kinds of functions. One could define
-- ∃-cong = Σ-cong Bijection.id, but the resulting "from" functions
-- would contain an unnecessary use of substitutivity, and I want to
-- avoid that.

private

  ∃-cong-impl :  {a b₁ b₂}
                  {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
                (∀ x  B₁ x  B₂ x)   B₁   B₂
  ∃-cong-impl B₁→B₂ = Σ-map id  {x}  B₁→B₂ x)

  ∃-cong-eq :  {a b₁ b₂}
                {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
              (∀ x  B₁ x  B₂ x)   B₁   B₂
  ∃-cong-eq B₁⇔B₂ = record
    { to   = ∃-cong-impl (to    B₁⇔B₂)
    ; from = ∃-cong-impl (from  B₁⇔B₂)
    } where open _⇔_

  ∃-cong-surj :  {a b₁ b₂}
                  {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
                (∀ x  B₁ x  B₂ x)   B₁   B₂
  ∃-cong-surj B₁↠B₂ = record
    { logical-equivalence = ∃-cong-eq (_↠_.logical-equivalence  B₁↠B₂)
    ; right-inverse-of    = uncurry λ x y 
        cong (_,_ x) (_↠_.right-inverse-of (B₁↠B₂ x) y)
    }

  ∃-cong-bij :  {a b₁ b₂}
                 {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
               (∀ x  B₁ x  B₂ x)   B₁   B₂
  ∃-cong-bij B₁↔B₂ = record
    { surjection      = ∃-cong-surj (_↔_.surjection  B₁↔B₂)
    ; left-inverse-of = uncurry λ x y 
        cong (_,_ x) (_↔_.left-inverse-of (B₁↔B₂ x) y)
    }

∃-cong :  {k a b₁ b₂}
           {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
         (∀ x  B₁ x ↝[ k ] B₂ x)   B₁ ↝[ k ]  B₂
∃-cong {implication}         = ∃-cong-impl
∃-cong {logical-equivalence} = ∃-cong-eq
∃-cong {injection}           = Σ-cong Bijection.id
∃-cong {embedding}           = Σ-preserves-embeddings Emb.id
∃-cong {surjection}          = ∃-cong-surj
∃-cong {bijection}           = ∃-cong-bij
∃-cong {equivalence}         = λ B₁≃B₂ 
  from-bijection $ ∃-cong-bij (from-equivalence  B₁≃B₂)

private

  -- ∃-cong also works for _×_, in which case it is a more general
  -- variant of id ×-cong_:

  ×-cong₂ :  {k a b₁ b₂}
              {A : Set a} {B₁ : Set b₁} {B₂ : Set b₂} 
           (A  B₁ ↝[ k ] B₂)  A × B₁ ↝[ k ] A × B₂
  ×-cong₂ = ∃-cong

-- The following lemma is a more general variant of _×-cong id.

×-cong₁ :  {k a₁ a₂ b}
            {A₁ : Set a₁} {A₂ : Set a₂} {B : Set b} 
          (B  A₁ ↝[ k ] A₂)  A₁ × B ↝[ k ] A₂ × B
×-cong₁ {A₁ = A₁} {A₂} {B} A₁↔A₂ =
  A₁ × B  ↔⟨ ×-comm 
  B × A₁  ↝⟨ ∃-cong A₁↔A₂ 
  B × A₂  ↔⟨ ×-comm ⟩□
  A₂ × B  

-- Lemmas that can be used to simplify sigma types where one of the
-- two type arguments is (conditionally) isomorphic to the unit type.

drop-⊤-right :  {k a b} {A : Set a} {B : A  Set b} 
               ((x : A)  B x ↔[ k ] )  Σ A B  A
drop-⊤-right {A = A} {B} B↔⊤ =
  Σ A B  ↔⟨ ∃-cong B↔⊤ 
  A ×   ↝⟨ ×-right-identity ⟩□
  A      

drop-⊤-left-× :  {k a b} {A : Set a} {B : Set b} 
                (B  A ↔[ k ] )  A × B  B
drop-⊤-left-× {A = A} {B} A↔⊤ =
  A × B  ↝⟨ ×-comm 
  B × A  ↝⟨ drop-⊤-right A↔⊤ ⟩□
  B      

drop-⊤-left-Σ :  {a b} {A : Set a} {B : A  Set b} 
                (A↔⊤ : A  ) 
                Σ A B  B (_↔_.from A↔⊤ tt)
drop-⊤-left-Σ {A = A} {B} A↔⊤ =
  Σ A B                   ↝⟨ inverse $ Σ-cong (inverse A↔⊤)  _  id) 
  Σ  (B  _↔_.from A↔⊤)  ↝⟨ Σ-left-identity ⟩□
  B (_↔_.from A↔⊤ tt)     

-- Currying.

currying :  {a b c} {A : Set a} {B : A  Set b} {C : Σ A B  Set c} 
           ((p : Σ A B)  C p)  ((x : A) (y : B x)  C (x , y))
currying = record
  { surjection = record
    { logical-equivalence = record { to = curry; from = uncurry }
    ; right-inverse-of    = refl
    }
  ; left-inverse-of = refl
  }

-- Some lemmas relating functions from binary sums and pairs of
-- functions.

Π⊎↠Π×Π :
   {a b c} {A : Set a} {B : Set b} {C : A  B  Set c} 
  ((x : A  B)  C x)
    
  ((x : A)  C (inj₁ x)) × ((y : B)  C (inj₂ y))
Π⊎↠Π×Π = record
  { logical-equivalence = record
    { to   = λ f  f  inj₁ , f  inj₂
    ; from = uncurry [_,_]
    }
  ; right-inverse-of = refl
  }

Π⊎↔Π×Π :
   {k a b c} {A : Set a} {B : Set b} {C : A  B  Set c} 
  Extensionality? k (a  b) c 
  ((x : A  B)  C x)
    ↝[ k ]
  ((x : A)  C (inj₁ x)) × ((y : B)  C (inj₂ y))
Π⊎↔Π×Π =
  generalise-ext? (_↠_.logical-equivalence Π⊎↠Π×Π) λ ext  record
    { surjection      = Π⊎↠Π×Π
    ; left-inverse-of = λ _  apply-ext ext [ refl  _ , refl  _ ]
    }

-- ∃ distributes "from the left" over _⊎_.

∃-⊎-distrib-left :
   {a b c} {A : Set a} {B : A  Set b} {C : A  Set c} 
  ( λ x  B x  C x)   B   C
∃-⊎-distrib-left = record
  { surjection = record
    { logical-equivalence = record
      { to   = uncurry λ x  [ inj₁  _,_ x , inj₂  _,_ x ]
      ; from = [ Σ-map id inj₁ , Σ-map id inj₂ ]
      }
    ; right-inverse-of = [ refl  inj₁ , refl  inj₂ ]
    }
  ; left-inverse-of =
      uncurry λ x  [ refl  _,_ x  inj₁ , refl  _,_ x  inj₂ ]
  }

-- ∃ also distributes "from the right" over _⊎_.

∃-⊎-distrib-right :
   {a b c} {A : Set a} {B : Set b} {C : A  B  Set c} 
  Σ (A  B) C  Σ A (C  inj₁)  Σ B (C  inj₂)
∃-⊎-distrib-right {A = A} {B} {C} = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = [ refl  inj₁ , refl  inj₂ ]
    }
  ; left-inverse-of = from∘to
  }
  where
  to : Σ (A  B) C  Σ A (C  inj₁)  Σ B (C  inj₂)
  to (inj₁ x , y) = inj₁ (x , y)
  to (inj₂ x , y) = inj₂ (x , y)

  from = [ Σ-map inj₁ id , Σ-map inj₂ id ]

  from∘to :  p  from (to p)  p
  from∘to (inj₁ x , y) = refl _
  from∘to (inj₂ x , y) = refl _

-- ∃ is "commutative".

∃-comm :  {a b c} {A : Set a} {B : Set b} {C : A  B  Set c} 
         ( λ x   λ y  C x y)  ( λ y   λ x  C x y)
∃-comm = record
  { surjection = record
    { logical-equivalence = record
      { to   = uncurry λ x  uncurry λ y z  (y , (x , z))
      ; from = uncurry λ x  uncurry λ y z  (y , (x , z))
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- One can introduce an existential by also introducing an equality.

∃-intro :  {a b} {A : Set a} (B : A  Set b) (x : A) 
          B x   λ y  B y × y  x
∃-intro B x =
  B x                    ↔⟨ inverse ×-right-identity 
  B x ×                 ↔⟨ id ×-cong inverse (_⇔_.to contractible⇔↔⊤ (singleton-contractible x)) 
  B x × ( λ y  y  x)  ↔⟨ ∃-comm 
  ( λ y  B x × y  x)  ↔⟨ ∃-cong  y  ×-cong₁  y≡x  subst  x  B x  B y) y≡x id)) ⟩□
  ( λ y  B y × y  x)  

-- A variant of ∃-intro.

∃-introduction :
   {a b} {A : Set a} {x : A} (B : (y : A)  x  y  Set b) 
  B x (refl x)   λ y   λ (x≡y : x  y)  B y x≡y
∃-introduction {x = x} B =
  B x (refl x)                                              ↝⟨ ∃-intro (uncurry B) _ 
  ( λ { (y , x≡y)  B y x≡y × (y , x≡y)  (x , refl x) })  ↝⟨ (∃-cong λ _  ∃-cong λ _ 
                                                                  _⇔_.to contractible⇔↔⊤ $
                                                                  mono₁ 0 (other-singleton-contractible x) _ _) 
  ( λ { (y , x≡y)  B y x≡y ×  })                         ↝⟨ (∃-cong λ _  ×-right-identity) 
  ( λ { (y , x≡y)  B y x≡y })                             ↝⟨ inverse Σ-assoc ⟩□
  ( λ y   λ x≡y  B y x≡y)                               

-- A non-dependent variant of Σ-≡,≡↔≡.
--
-- This property used to be defined in terms of Σ-≡,≡↔≡, but was
-- changed in order to make it compute in a different way.

≡×≡↔≡ :  {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} 
        (proj₁ p₁  proj₁ p₂ × proj₂ p₁  proj₂ p₂)  (p₁  p₂)
≡×≡↔≡ {B = B} {p₁} {p₂} = record
  { surjection = record
    { logical-equivalence = record
      { to   = uncurry (cong₂ _,_)
      ; from = λ eq  cong proj₁ eq , cong proj₂ eq
      }
    ; right-inverse-of = λ eq 
        cong₂ _,_ (cong proj₁ eq) (cong proj₂ eq)  ≡⟨ cong₂-cong-cong _ _ _,_ 
        cong  p  proj₁ p , proj₂ p) eq          ≡⟨⟩
        cong id eq                                 ≡⟨ sym $ cong-id _ ⟩∎
        eq                                         
    }
  ; left-inverse-of = λ { (eq₁ , eq₂) 
        cong proj₁ (cong₂ _,_ eq₁ eq₂) , cong proj₂ (cong₂ _,_ eq₁ eq₂)  ≡⟨ cong₂ _,_ (cong-proj₁-cong₂-, eq₁ eq₂) (cong-proj₂-cong₂-, eq₁ eq₂) ⟩∎
        eq₁ , eq₂                                                        
      }
  }

-- If one is given an equality between pairs, where the second
-- components of the pairs are propositional, then one can restrict
-- attention to the first components.

ignore-propositional-component :
   {a b} {A : Set a} {B : A  Set b} {p q : Σ A B} 
  Is-proposition (B (proj₁ q)) 
  (proj₁ p  proj₁ q)  (p  q)
ignore-propositional-component {B = B} {p₁ , p₂} {q₁ , q₂} Bq₁-prop =
  (p₁  q₁)                                  ↝⟨ inverse ×-right-identity 
  (p₁  q₁ × )                              ↝⟨ ∃-cong  _  inverse $ _⇔_.to contractible⇔↔⊤ (Bq₁-prop _ _)) 
  ( λ (eq : p₁  q₁)  subst B eq p₂  q₂)  ↝⟨ Bijection.Σ-≡,≡↔≡ ⟩□
  ((p₁ , p₂)  (q₁ , q₂))                    

-- Contractible commutes with _×_ (assuming extensionality).

Contractible-commutes-with-× :
   {x y} {X : Set x} {Y : Set y} 
  Extensionality (x  y) (x  y) 
  Contractible (X × Y)  (Contractible X × Contractible Y)
Contractible-commutes-with-× {x} {y} ext =
  _↔_.to (Eq.⇔↔≃ ext
                 (Contractible-propositional ext)
                 (×-closure 1 (Contractible-propositional
                                 (lower-extensionality y y ext))
                              (Contractible-propositional
                                 (lower-extensionality x x ext))))
    (record
       { to = λ cX×Y 
           lemma cX×Y ,
           lemma (H-level.respects-surjection
                    (_↔_.surjection ×-comm) 0 cX×Y)
       ; from = λ { ((x , eq₁) , (y , eq₂)) 
           (x , y) ,
           λ { (x′ , y′) 
             (x  , y)   ≡⟨ cong₂ _,_ (eq₁ x′) (eq₂ y′) ⟩∎
             (x′ , y′)   } }
       })
  where
  lemma :  {x y} {X : Set x} {Y : Set y} 
          Contractible (X × Y)  Contractible X
  lemma ((x , y) , eq) = x , λ x′ 
    x               ≡⟨⟩
    proj₁ (x , y)   ≡⟨ cong proj₁ (eq (x′ , y)) ⟩∎
    proj₁ (x′ , y)  

------------------------------------------------------------------------
-- Some lemmas related to _≃_

-- Equality of equivalences is isomorphic to pointwise equality of the
-- underlying functions (assuming extensionality).

≃-to-≡↔≡ :
   {a b} 
  Extensionality (a  b) (a  b) 
  {A : Set a} {B : Set b} {p q : A  B} 
  (∀ x  _≃_.to p x  _≃_.to q x)  p  q
≃-to-≡↔≡ {a} {b} ext {p = p} {q} =
  (∀ x  _≃_.to p x  _≃_.to q x)                                        ↔⟨ Eq.extensionality-isomorphism (lower-extensionality b a ext) 
  _≃_.to p  _≃_.to q                                                    ↝⟨ ignore-propositional-component (Eq.propositional ext _) 
  (_≃_.to p , _≃_.is-equivalence p)  (_≃_.to q , _≃_.is-equivalence q)  ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ Eq.≃-as-Σ) ⟩□
  p  q                                                                  

-- Equality of bijections between a set and a type is isomorphic to
-- pointwise equality of the underlying functions (assuming
-- extensionality).

↔-to-≡↔≡ :
   {a b} 
  Extensionality (a  b) (a  b) 
  {A : Set a} {B : Set b} {p q : A  B} 
  Is-set A 
  (∀ x  _↔_.to p x  _↔_.to q x)  p  q
↔-to-≡↔≡ ext {p = p} {q} A-set =
  (∀ x  _↔_.to p x  _↔_.to q x)                    ↝⟨ id 
  (∀ x  _≃_.to (Eq.↔⇒≃ p) x  _≃_.to (Eq.↔⇒≃ q) x)  ↝⟨ ≃-to-≡↔≡ ext 
  Eq.↔⇒≃ p  Eq.↔⇒≃ q                                ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ (Eq.↔↔≃ ext A-set)) ⟩□
  p  q                                              

-- Equality of equivalences is isomorphic to pointwise equality of the
-- underlying /inverse/ functions (assuming extensionality).

≃-from-≡↔≡ :
   {a b} 
  Extensionality (a  b) (a  b) 
  {A : Set a} {B : Set b} {p q : A  B} 
  (∀ x  _≃_.from p x  _≃_.from q x)  p  q
≃-from-≡↔≡ ext {p = p} {q} =
  (∀ x  _≃_.from p x  _≃_.from q x)  ↝⟨ ≃-to-≡↔≡ ext 
  inverse p  inverse q                ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ (Eq.inverse-isomorphism ext)) ⟩□
  p  q                                

-- Equality of bijections between a set and a type is isomorphic to
-- pointwise equality of the underlying /inverse/ functions (assuming
-- extensionality).

↔-from-≡↔≡ :
   {a b} 
  Extensionality (a  b) (a  b) 
  {A : Set a} {B : Set b} {p q : A  B} 
  Is-set A 
  (∀ x  _↔_.from p x  _↔_.from q x)  p  q
↔-from-≡↔≡ ext {p = p} {q} A-set =
  (∀ x  _↔_.from p x  _↔_.from q x)                    ↝⟨ id 
  (∀ x  _≃_.from (Eq.↔⇒≃ p) x  _≃_.from (Eq.↔⇒≃ q) x)  ↝⟨ ≃-from-≡↔≡ ext 
  Eq.↔⇒≃ p  Eq.↔⇒≃ q                                    ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ (Eq.↔↔≃ ext A-set)) ⟩□
  p  q                                                  

-- Contractibility is isomorphic to equivalence to the unit type
-- (assuming extensionality).

contractible↔≃⊤ :
   {a} {A : Set a} 
  Extensionality a a 
  Contractible A  (A  )
contractible↔≃⊤ ext = record
  { surjection = record
    { logical-equivalence = record
      { to   = Eq.↔⇒≃  _⇔_.to contractible⇔↔⊤
      ; from = _⇔_.from contractible⇔↔⊤  _≃_.bijection
      }
    ; right-inverse-of = λ _ 
        Eq.lift-equality ext (refl _)
    }
  ; left-inverse-of = λ _ 
      _⇔_.to propositional⇔irrelevant
        (Contractible-propositional ext) _ _
  }

-- Equivalence to the empty type is equivalent to not being inhabited
-- (assuming extensionality).

≃⊥≃¬ :
   {a } {A : Set a} 
  Extensionality (a  ) (a  ) 
  (A   { = })  (¬ A)
≃⊥≃¬ { = } {A} ext =
  _↔_.to (Eq.⇔↔≃ ext (Eq.right-closure ext 0 ⊥-propositional)
                     (¬-propositional
                        (lower-extensionality  _ ext))) (record
    { to   = λ eq a  ⊥-elim (_≃_.to eq a)
    ; from = λ ¬a  A  ↔⟨ inverse (Bijection.⊥↔uninhabited ¬a) ⟩□
                      
    })

------------------------------------------------------------------------
-- _⊎_ and _×_ form a commutative semiring

-- _×_ distributes from the left over _⊎_.

×-⊎-distrib-left :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
                   A × (B  C)  (A × B)  (A × C)
×-⊎-distrib-left = ∃-⊎-distrib-left

-- _×_ distributes from the right over _⊎_.

×-⊎-distrib-right :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
                    (A  B) × C  (A × C)  (B × C)
×-⊎-distrib-right = ∃-⊎-distrib-right

------------------------------------------------------------------------
-- Some lemmas related to functions

-- The non-dependent function space preserves non-dependent functions
-- (contravariantly for the domain).

→-cong-→ :  {a b c d}
             {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
           (B  A)  (C  D)  (A  C)  (B  D)
→-cong-→ B→A C→D = (C→D ∘_)  (_∘ B→A)

private

  -- A lemma used in the implementations of →-cong and →-cong-↠.

  →-cong-⇔ :  {a b c d}
               {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
             A  B  C  D  (A  C)  (B  D)
  →-cong-⇔ A⇔B C⇔D = record
    { to   = →-cong-→ (from A⇔B) (to   C⇔D)
    ; from = →-cong-→ (to   A⇔B) (from C⇔D)
    }
    where open _⇔_

-- The non-dependent function space preserves split surjections
-- (assuming extensionality).

→-cong-↠ :  {a b c d}  Extensionality b d 
           {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
           A  B  C  D  (A  C)  (B  D)
→-cong-↠ {a} {b} {c} {d} ext A↠B C↠D = record
  { logical-equivalence = logical-equiv
  ; right-inverse-of    = right-inv
  }
  where
  open _↠_

  logical-equiv = →-cong-⇔ (_↠_.logical-equivalence A↠B)
                           (_↠_.logical-equivalence C↠D)

  abstract
    right-inv :
       f  _⇔_.to logical-equiv (_⇔_.from logical-equiv f)  f
    right-inv f = apply-ext ext λ x 
      to C↠D (from C↠D (f (to A↠B (from A↠B x))))  ≡⟨ right-inverse-of C↠D _ 
      f (to A↠B (from A↠B x))                      ≡⟨ cong f $ right-inverse-of A↠B _ ⟩∎
      f x                                          

private

  -- A lemma used in the implementation of →-cong.

  →-cong-↔ :  {a b c d}
               {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
             Extensionality (a  b) (c  d) 
             A  B  C  D  (A  C)  (B  D)
  →-cong-↔ {a} {b} {c} {d} ext A↔B C↔D = record
    { surjection      = surj
    ; left-inverse-of = left-inv
    }
    where
    open _↔_

    surj = →-cong-↠ (lower-extensionality a c ext)
                    (_↔_.surjection A↔B)
                    (_↔_.surjection C↔D)

    abstract
      left-inv :
         f  _↠_.from surj (_↠_.to surj f)  f
      left-inv f = apply-ext (lower-extensionality b d ext) λ x 
        from C↔D (to C↔D (f (from A↔B (to A↔B x))))  ≡⟨ left-inverse-of C↔D _ 
        f (from A↔B (to A↔B x))                      ≡⟨ cong f $ left-inverse-of A↔B _ ⟩∎
        f x                                          

-- The non-dependent function space preserves symmetric kinds of
-- functions (in some cases assuming extensionality).

→-cong :  {k a b c d} 
         Extensionality?  k ⌋-sym (a  b) (c  d) 
         {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
         A ↝[  k ⌋-sym ] B  C ↝[  k ⌋-sym ] D 
         (A  C) ↝[  k ⌋-sym ] (B  D)
→-cong {logical-equivalence} _   A⇔B C⇔D = →-cong-⇔ A⇔B C⇔D
→-cong {bijection}           ext A↔B C↔D = →-cong-↔ ext A↔B C↔D
→-cong {equivalence}         ext A≃B C≃D = record
  { to             = to
  ; is-equivalence = λ y 
      ((from y , right-inverse-of y) , irrelevance y)
  }
  where
  A→B≃C→D =
    Eq.↔⇒≃ (→-cong-↔ ext (_≃_.bijection A≃B) (_≃_.bijection C≃D))

  to   = _≃_.to   A→B≃C→D
  from = _≃_.from A→B≃C→D

  abstract
    right-inverse-of :  x  to (from x)  x
    right-inverse-of = _≃_.right-inverse-of A→B≃C→D

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

private

  -- Lemmas used in the implementation of ∀-cong.

  ∀-cong-→ :
     {a b₁ b₂} {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
    (∀ x  B₁ x  B₂ x) 
    ((x : A)  B₁ x)  ((x : A)  B₂ x)
  ∀-cong-→ B₁→B₂ = B₁→B₂ _ ⊚_

  ∀-cong-⇔ :
     {a b₁ b₂} {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
    (∀ x  B₁ x  B₂ x) 
    ((x : A)  B₁ x)  ((x : A)  B₂ x)
  ∀-cong-⇔ B₁⇔B₂ = record
    { to   = ∀-cong-→ (_⇔_.to    B₁⇔B₂)
    ; from = ∀-cong-→ (_⇔_.from  B₁⇔B₂)
    }

  ∀-cong-surj :
     {a b₁ b₂} 
    Extensionality a (b₁  b₂) 
    {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
    (∀ x  B₁ x  B₂ x) 
    ((x : A)  B₁ x)  ((x : A)  B₂ x)
  ∀-cong-surj {b₁ = b₁} ext B₁↠B₂ = record
    { logical-equivalence = equiv
    ; right-inverse-of    = right-inverse-of
    }
    where
    equiv = ∀-cong-⇔ (_↠_.logical-equivalence  B₁↠B₂)

    abstract
      right-inverse-of :  f  _⇔_.to equiv (_⇔_.from equiv f)  f
      right-inverse-of = λ f 
        apply-ext (lower-extensionality lzero b₁ ext) λ x 
          _↠_.to (B₁↠B₂ x) (_↠_.from (B₁↠B₂ x) (f x))  ≡⟨ _↠_.right-inverse-of (B₁↠B₂ x) (f x) ⟩∎
          f x                                          

  ∀-cong-bij :
     {a b₁ b₂} 
    Extensionality a (b₁  b₂) 
    {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
    (∀ x  B₁ x  B₂ x) 
    ((x : A)  B₁ x)  ((x : A)  B₂ x)
  ∀-cong-bij {b₂ = b₂} ext B₁↔B₂ = record
    { surjection      = surj
    ; left-inverse-of = left-inverse-of
    }
    where
    surj = ∀-cong-surj ext (_↔_.surjection  B₁↔B₂)

    abstract
      left-inverse-of :  f  _↠_.from surj (_↠_.to surj f)  f
      left-inverse-of = λ f 
        apply-ext (lower-extensionality lzero b₂ ext) λ x 
          _↔_.from (B₁↔B₂ x) (_↔_.to (B₁↔B₂ x) (f x))  ≡⟨ _↔_.left-inverse-of (B₁↔B₂ x) (f x) ⟩∎
          f x                                          

  ∀-cong-eq :
     {a b₁ b₂} 
    Extensionality a (b₁  b₂) 
    {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
    (∀ x  B₁ x  B₂ x) 
    ((x : A)  B₁ x)  ((x : A)  B₂ x)
  ∀-cong-eq ext = Eq.↔⇒≃  ∀-cong-bij ext  (_≃_.bijection ⊚_)

  ∀-cong-inj :
     {a b₁ b₂} 
    Extensionality a (b₁  b₂) 
    {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
    (∀ x  B₁ x  B₂ x) 
    ((x : A)  B₁ x)  ((x : A)  B₂ x)
  ∀-cong-inj {b₁ = b₁} {b₂} ext B₁↣B₂ = record
    { to        = to
    ; injective = injective
    }
    where
    to = ∀-cong-→ (_↣_.to  B₁↣B₂)

    abstract
      injective : Injective to
      injective {x = f} {y = g} =
         x  _↣_.to (B₁↣B₂ x) (f x))   x  _↣_.to (B₁↣B₂ x) (g x))  ↔⟨ inverse $ Eq.extensionality-isomorphism
                                                                                        (lower-extensionality lzero b₁ ext) 
        (∀ x  _↣_.to (B₁↣B₂ x) (f x)  _↣_.to (B₁↣B₂ x) (g x))          ↝⟨ ∀-cong-→  x  _↣_.injective (B₁↣B₂ x)) 
        (∀ x  f x  g x)                                                ↔⟨ Eq.extensionality-isomorphism
                                                                              (lower-extensionality lzero b₂ ext) ⟩□
        f  g                                                            

  ∀-cong-emb :
     {a b₁ b₂} 
    Extensionality a (b₁  b₂) 
    {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
    (∀ x  Embedding (B₁ x) (B₂ x)) 
    Embedding ((x : A)  B₁ x) ((x : A)  B₂ x)
  ∀-cong-emb {b₁ = b₁} {b₂} ext B₁↣B₂ = record
    { to           = to
    ; is-embedding = is-embedding
    }
    where
    to = ∀-cong-→ (Embedding.to  B₁↣B₂)

    ext₂ = lower-extensionality lzero b₁ ext

    abstract
      is-embedding : Is-embedding to
      is-embedding f g = _≃_.is-equivalence $
        Eq.with-other-function
          (f  g                                   ↝⟨ inverse $ Eq.extensionality-isomorphism
                                                                  (lower-extensionality lzero b₂ ext) 
           (∀ x  f x  g x)                       ↝⟨ ∀-cong-eq ext  x 
                                                        Eq.⟨ _ , Embedding.is-embedding (B₁↣B₂ x) (f x) (g x) ) 
           (∀ x  Embedding.to (B₁↣B₂ x) (f x) 
                  Embedding.to (B₁↣B₂ x) (g x))    ↝⟨ Eq.extensionality-isomorphism ext₂ ⟩□

            x  Embedding.to (B₁↣B₂ x) (f x)) 
            x  Embedding.to (B₁↣B₂ x) (g x))    )
          _
           f≡g 
             apply-ext (Eq.good-ext ext₂)
                x  cong (Embedding.to (B₁↣B₂ x)) (ext⁻¹ f≡g x))        ≡⟨⟩

             apply-ext (Eq.good-ext ext₂)
                x  cong (Embedding.to (B₁↣B₂ x)) (cong (_$ x) f≡g))    ≡⟨ cong (apply-ext (Eq.good-ext ext₂)) (apply-ext ext₂ λ _ 
                                                                               cong-∘ _ _ _) 
             apply-ext (Eq.good-ext ext₂)
                x  cong  h  Embedding.to (B₁↣B₂ x) (h x)) f≡g)      ≡⟨ cong (apply-ext (Eq.good-ext ext₂)) (apply-ext ext₂ λ _  sym $
                                                                               cong-∘ _ _ _) 
             apply-ext (Eq.good-ext ext₂)
                x  cong (_$ x)
                        (cong  h x  Embedding.to (B₁↣B₂ x) (h x))
                           f≡g))                                          ≡⟨⟩

             apply-ext (Eq.good-ext ext₂)
               (ext⁻¹ (cong  h x  Embedding.to (B₁↣B₂ x) (h x)) f≡g))  ≡⟨ _≃_.right-inverse-of (Eq.extensionality-isomorphism ext₂) _ ⟩∎

             cong  h x  Embedding.to (B₁↣B₂ x) (h x)) f≡g              )

-- Π preserves all kinds of functions in its second argument (in some
-- cases assuming extensionality).

∀-cong :
   {k a b₁ b₂} 
  Extensionality? k a (b₁  b₂) 
  {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
  (∀ x  B₁ x ↝[ k ] B₂ x) 
  ((x : A)  B₁ x) ↝[ k ] ((x : A)  B₂ x)
∀-cong {implication}         = λ _  ∀-cong-→
∀-cong {logical-equivalence} = λ _  ∀-cong-⇔
∀-cong {injection}           = ∀-cong-inj
∀-cong {embedding}           = ∀-cong-emb
∀-cong {surjection}          = ∀-cong-surj
∀-cong {bijection}           = ∀-cong-bij
∀-cong {equivalence}         = ∀-cong-eq

-- The implicit variant of Π preserves all kinds of functions in its
-- second argument (in some cases assuming extensionality).

implicit-∀-cong :
   {k a b₁ b₂} 
  Extensionality? k a (b₁  b₂) 
  {A : Set a} {B₁ : A  Set b₁} {B₂ : A  Set b₂} 
  (∀ {x}  B₁ x ↝[ k ] B₂ x) 
  ({x : A}  B₁ x) ↝[ k ] ({x : A}  B₂ x)
implicit-∀-cong ext {A} {B₁} {B₂} B₁↝B₂ =
  ({x : A}  B₁ x)  ↔⟨ Bijection.implicit-Π↔Π 
  ((x : A)  B₁ x)  ↝⟨ ∀-cong ext  _  B₁↝B₂) 
  ((x : A)  B₂ x)  ↔⟨ inverse Bijection.implicit-Π↔Π ⟩□
  ({x : A}  B₂ x)  

-- Two generalisations of ∀-cong for non-dependent functions.

Π-cong-contra-→ :
   {a₁ a₂ b₁ b₂}
    {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
  (A₂→A₁ : A₂  A₁) 
  (∀ x  B₁ (A₂→A₁ x)  B₂ x) 
  ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
Π-cong-contra-→ {B₁ = B₁} {B₂} A₂→A₁ B₁→B₂ f x =
                $⟨ f (A₂→A₁ x) 
  B₁ (A₂→A₁ x)  ↝⟨ B₁→B₂ x 
  B₂ x          

Π-cong-→ :
   {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)) 
  ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
Π-cong-→ {B₁ = B₁} {B₂} A₁↠A₂ B₁→B₂ f x =
                                        $⟨ f (_↠_.from A₁↠A₂ x) 
  B₁ (_↠_.from A₁↠A₂ x)                 ↝⟨ B₁→B₂ (_↠_.from A₁↠A₂ x) 
  B₂ (_↠_.to A₁↠A₂ (_↠_.from A₁↠A₂ x))  ↝⟨ subst B₂ (_↠_.right-inverse-of A₁↠A₂ x) ⟩□
  B₂ x                                  

-- Two generalisations of ∀-cong for logical equivalences.

Π-cong-⇔ :
   {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)) 
  ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
Π-cong-⇔ {A₁ = A₁} {A₂} {B₁} {B₂} A₁↠A₂ B₁⇔B₂ = record
  { to   = Π-cong-→                A₁↠A₂  (_⇔_.to    B₁⇔B₂)
  ; from = Π-cong-contra-→ (_↠_.to A₁↠A₂) (_⇔_.from  B₁⇔B₂)
  }

Π-cong-contra-⇔ :
   {a₁ a₂ b₁ b₂}
    {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
  (A₂↠A₁ : A₂  A₁) 
  (∀ x  B₁ (_↠_.to A₂↠A₁ x)  B₂ x) 
  ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
Π-cong-contra-⇔ {A₁ = A₁} {A₂} {B₁} {B₂} A₂↠A₁ B₁⇔B₂ = record
  { to   = Π-cong-contra-→ (_↠_.to A₂↠A₁) (_⇔_.to    B₁⇔B₂)
  ; from = Π-cong-→                A₂↠A₁  (_⇔_.from  B₁⇔B₂)
  }

-- A generalisation of ∀-cong for split surjections.

Π-cong-↠ :
   {a₁ a₂ 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)
Π-cong-↠ ext {B₂ = B₂} A₁↠A₂ B₁↠B₂ = record
  { logical-equivalence = equiv
  ; right-inverse-of    = to∘from
  }
  where
  equiv = Π-cong-⇔ A₁↠A₂ (_↠_.logical-equivalence  B₁↠B₂)

  abstract

    to∘from :  f  _⇔_.to equiv (_⇔_.from equiv f)  f
    to∘from f = apply-ext 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)))          ≡⟨ dependent-cong f _ ⟩∎

      f x                                              

-- A generalisation of ∀-cong for injections.

Π-cong-contra-↣ :
   {a₁ a₂ 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₁ (_↠_.to A₂↠A₁ x)  B₂ x) 
  ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
Π-cong-contra-↣ ext A₂↠A₁ B₁↣B₂ = record
  { to        = to
  ; injective = injective
  }
  where
  to = Π-cong-contra-→ (_↠_.to A₂↠A₁) (_↣_.to  B₁↣B₂)

  abstract

    injective : Injective to
    injective {x = f} {y = g} to-f≡to-g = apply-ext ext λ x 

      let x′ = _↠_.to A₂↠A₁ (_↠_.from A₂↠A₁ x) in
                                                       $⟨ to-f≡to-g 
       x  _↣_.to (B₁↣B₂ x) (f (_↠_.to A₂↠A₁ x))) 
       x  _↣_.to (B₁↣B₂ x) (g (_↠_.to A₂↠A₁ x)))    ↝⟨ cong (_$ _) 

      _↣_.to (B₁↣B₂ (_↠_.from A₂↠A₁ x)) (f x′) 
      _↣_.to (B₁↣B₂ (_↠_.from A₂↠A₁ x)) (g x′)         ↝⟨ _↣_.injective (B₁↣B₂ _) 

      f x′  g x′                                      ↝⟨ subst  x  f x  g x) $ _↠_.right-inverse-of A₂↠A₁ x ⟩□

      f x  g x                                        

private

  -- Lemmas used in the implementations of Π-cong and Π-cong-contra.

  Π-cong-contra-↠ :
     {a₁ a₂ 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₁ (_≃_.to A₂≃A₁ x)  B₂ x) 
    ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
  Π-cong-contra-↠ ext {B₁ = B₁} A₂≃A₁ B₁↠B₂ = record
    { logical-equivalence = equiv
    ; right-inverse-of    = to∘from
    }
    where
    equiv = Π-cong-contra-⇔ (_≃_.surjection A₂≃A₁)
                            (_↠_.logical-equivalence  B₁↠B₂)

    abstract

      to∘from :  f  _⇔_.to equiv (_⇔_.from equiv f)  f
      to∘from f = apply-ext ext λ x 
        _↠_.to (B₁↠B₂ x)
          (subst B₁ (_≃_.right-inverse-of A₂≃A₁ (_≃_.to A₂≃A₁ x))
             (_↠_.from (B₁↠B₂ (_≃_.from A₂≃A₁ (_≃_.to A₂≃A₁ x)))
                (f (_≃_.from A₂≃A₁ (_≃_.to A₂≃A₁ x)))))                  ≡⟨ cong  eq  _↠_.to (B₁↠B₂ x) (subst B₁ eq _)) $ sym $
                                                                              _≃_.left-right-lemma A₂≃A₁ _ 
        _↠_.to (B₁↠B₂ x)
          (subst B₁ (cong (_≃_.to A₂≃A₁) $ _≃_.left-inverse-of A₂≃A₁ x)
             (_↠_.from (B₁↠B₂ (_≃_.from A₂≃A₁ (_≃_.to A₂≃A₁ x)))
                (f (_≃_.from A₂≃A₁ (_≃_.to A₂≃A₁ x)))))                  ≡⟨ cong (_↠_.to (B₁↠B₂ x)) $ sym $ subst-∘ _ _ _ 

        _↠_.to (B₁↠B₂ x)
          (subst (B₁  _≃_.to A₂≃A₁) (_≃_.left-inverse-of A₂≃A₁ x)
             (_↠_.from (B₁↠B₂ (_≃_.from A₂≃A₁ (_≃_.to A₂≃A₁ x)))
                (f (_≃_.from A₂≃A₁ (_≃_.to A₂≃A₁ x)))))                  ≡⟨ cong (_↠_.to (B₁↠B₂ x)) $
                                                                              dependent-cong  x  _↠_.from (B₁↠B₂ x) (f x)) _ 

        _↠_.to (B₁↠B₂ x) (_↠_.from (B₁↠B₂ x) (f x))                      ≡⟨ _↠_.right-inverse-of (B₁↠B₂ x) _ ⟩∎

        f x                                                              

  Π-cong-↔ :
     {a₁ a₂ b₁ b₂} 
    Extensionality (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)) 
    ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
  Π-cong-↔ {a₁} {a₂} {b₁} {b₂} ext {B₂ = B₂} A₁≃A₂ B₁↔B₂ = record
    { surjection      = surj
    ; left-inverse-of = from∘to
    }
    where
    surj = Π-cong-↠ (lower-extensionality a₁ b₁ ext)
                    (_≃_.surjection A₁≃A₂) (_↔_.surjection  B₁↔B₂)

    abstract

      from∘to :  f  _↠_.from surj (_↠_.to surj f)  f
      from∘to =
        _↠_.right-inverse-of $
          Π-cong-contra-↠ (lower-extensionality a₂ b₂ ext)
                          {B₁ = B₂}
                          A₁≃A₂
                          (_↔_.surjection  inverse  B₁↔B₂)

  Π-cong-contra-↔ :
     {a₁ a₂ b₁ b₂} 
    Extensionality (a₁  a₂) (b₁  b₂) 
     {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
    (A₂≃A₁ : A₂  A₁) 
    (∀ x  B₁ (_≃_.to A₂≃A₁ x)  B₂ x) 
    ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
  Π-cong-contra-↔ {a₁} {a₂} {b₁} {b₂} ext {B₂ = B₂} A₂≃A₁ B₁↔B₂ = record
    { surjection      = surj
    ; left-inverse-of = from∘to
    }
    where
    surj = Π-cong-contra-↠ (lower-extensionality a₁ b₁ ext)
                           A₂≃A₁ (_↔_.surjection  B₁↔B₂)

    abstract

      from∘to :  f  _↠_.from surj (_↠_.to surj f)  f
      from∘to =
        _↠_.right-inverse-of $
          Π-cong-↠ (lower-extensionality a₂ b₂ ext)
                   (_≃_.surjection A₂≃A₁)
                   (_↔_.surjection  inverse  B₁↔B₂)

  Π-cong-≃ :
     {a₁ a₂ b₁ b₂} 
    Extensionality (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)) 
    ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
  Π-cong-≃ ext A₁≃A₂ =
    from-isomorphism  Π-cong-↔ ext A₁≃A₂  (from-isomorphism ⊚_)

  Π-cong-contra-≃ :
     {a₁ a₂ b₁ b₂} 
    Extensionality (a₁  a₂) (b₁  b₂) 
     {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
    (A₂≃A₁ : A₂  A₁) 
    (∀ x  B₁ (_≃_.to A₂≃A₁ x)  B₂ x) 
    ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)
  Π-cong-contra-≃ ext A₂≃A₁ =
    from-isomorphism  Π-cong-contra-↔ ext A₂≃A₁  (from-isomorphism ⊚_)

  Π-cong-↣ :
     {a₁ a₂ 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)
  Π-cong-↣ ext {A₁} {A₂} {B₁} {B₂} A₁≃A₂ =
    (∀ x  B₁ x  B₂ (_≃_.to A₁≃A₂ x))                                    ↝⟨ Π-cong-contra-→ (_≃_.from A₁≃A₂)  _  id) 
    (∀ x  B₁ (_≃_.from A₁≃A₂ x)  B₂ (_≃_.to A₁≃A₂ (_≃_.from A₁≃A₂ x)))  ↝⟨ (∀-cong _ λ _ 
                                                                              subst ((B₁ _ ↣_)  B₂) (_≃_.right-inverse-of A₁≃A₂ _)) 
    (∀ x  B₁ (_≃_.from A₁≃A₂ x)  B₂ x)                                  ↝⟨ Π-cong-contra-↣ ext (_≃_.surjection $ inverse A₁≃A₂) ⟩□
    ((x : A₁)  B₁ x)  ((x : A₂)  B₂ x)                                 

  Π-cong-contra-Emb :
     {a₁ a₂ b₁ b₂} 
    Extensionality (a₁  a₂) (b₁  b₂) 
     {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
    (A₂≃A₁ : A₂  A₁) 
    (∀ x  Embedding (B₁ (_≃_.to A₂≃A₁ x)) (B₂ x)) 
    Embedding ((x : A₁)  B₁ x) ((x : A₂)  B₂ x)
  Π-cong-contra-Emb {a₁} {a₂} {b₁} {b₂} ext A₂≃A₁ B₁↣B₂ = record
    { to           = to
    ; is-embedding = is-embedding
    }
    where

    to = Π-cong-contra-→ (_≃_.to A₂≃A₁) (Embedding.to  B₁↣B₂)

    abstract

      ext₁₁ : Extensionality a₁ b₁
      ext₁₁ = lower-extensionality a₂ b₂ ext

      ext₂₁ : Extensionality a₂ b₁
      ext₂₁ = lower-extensionality a₁ b₂ ext

      ext₂₂ : Extensionality a₂ b₂
      ext₂₂ = lower-extensionality a₁ b₁ ext

      is-embedding : Is-embedding to
      is-embedding f g =
        _≃_.is-equivalence $
          Eq.with-other-function
            (f  g                                                  ↝⟨ inverse $ Eq.extensionality-isomorphism ext₁₁ 

             (∀ x  f x  g x)                                      ↝⟨ (inverse $ Π-cong-≃ ext A₂≃A₁ λ x 
                                                                        inverse $ Embedding.equivalence (B₁↣B₂ x)) 
             (∀ x  Embedding.to (B₁↣B₂ x) (f (_≃_.to A₂≃A₁ x)) 
                    Embedding.to (B₁↣B₂ x) (g (_≃_.to A₂≃A₁ x)))    ↝⟨ Eq.extensionality-isomorphism ext₂₂ 

              {x}  Embedding.to (B₁↣B₂ x))  f  _≃_.to A₂≃A₁ 
              {x}  Embedding.to (B₁↣B₂ x))  g  _≃_.to A₂≃A₁    ↔⟨⟩

             to f  to g                                            )
            _
             f≡g 
               apply-ext (Eq.good-ext ext₂₂)
                 (cong (Embedding.to (B₁↣B₂ _)) 
                    ext⁻¹ f≡g  _≃_.to A₂≃A₁)                       ≡⟨ sym $ Eq.cong-post-∘-good-ext ext₂₁ ext₂₂ _ 

               cong (Embedding.to (B₁↣B₂ _) ⊚_)
                 (apply-ext (Eq.good-ext ext₂₁)
                    (ext⁻¹ f≡g  _≃_.to A₂≃A₁))                     ≡⟨ cong (cong (Embedding.to (B₁↣B₂ _) ⊚_)) $ sym $
                                                                       Eq.cong-pre-∘-good-ext ext₂₁ ext₁₁ _ 
               cong (Embedding.to (B₁↣B₂ _) ⊚_)
                 (cong (_⊚ _≃_.to A₂≃A₁)
                   (apply-ext (Eq.good-ext ext₁₁) (ext⁻¹ f≡g)))     ≡⟨ cong-∘ _ _ _ 

               cong to (apply-ext (Eq.good-ext ext₁₁) (ext⁻¹ f≡g))  ≡⟨ cong (cong to) $
                                                                       _≃_.right-inverse-of (Eq.extensionality-isomorphism ext₁₁) _ ⟩∎

               cong to f≡g                                          )

  Π-cong-Emb :
     {a₁ a₂ b₁ b₂} 
    Extensionality (a₁  a₂) (b₁  b₂) 
     {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
    (A₁≃A₂ : A₁  A₂) 
    (∀ x  Embedding (B₁ x) (B₂ (_≃_.to A₁≃A₂ x))) 
    Embedding ((x : A₁)  B₁ x) ((x : A₂)  B₂ x)
  Π-cong-Emb ext {A₁} {A₂} {B₁} {B₂} A₁≃A₂ =

    (∀ x  Embedding (B₁ x) (B₂ (_≃_.to A₁≃A₂ x)))            ↝⟨ Π-cong-contra-→ (_≃_.from A₁≃A₂)  _  id) 

    (∀ x  Embedding (B₁ (_≃_.from A₁≃A₂ x))
                     (B₂ (_≃_.to A₁≃A₂ (_≃_.from A₁≃A₂ x))))  ↝⟨ (∀-cong _ λ _  subst (Embedding (B₁ _)  B₂) (_≃_.right-inverse-of A₁≃A₂ _)) 

    (∀ x  Embedding (B₁ (_≃_.from A₁≃A₂ x)) (B₂ x))          ↝⟨ Π-cong-contra-Emb ext (inverse A₁≃A₂) ⟩□

    Embedding ((x : A₁)  B₁ x) ((x : A₂)  B₂ x)             

-- A generalisation of ∀-cong.

Π-cong :
   {k₁ k₂ a₁ a₂ b₁ b₂} 
  Extensionality? k₂ (a₁  a₂) (b₁  b₂) 
  {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
  (A₁↔A₂ : A₁ ↔[ k₁ ] A₂) 
  (∀ x  B₁ x ↝[ k₂ ] B₂ (to-implication A₁↔A₂ x)) 
  ((x : A₁)  B₁ x) ↝[ k₂ ] ((x : A₂)  B₂ x)
Π-cong {k₁} {k₂} {a₁} {a₂} {b₁} {b₂}
       ext {A₁} {A₂} {B₁} {B₂} A₁↔A₂ B₁↝B₂ =
  helper k₂ ext (B₁↝B₂′ k₁ A₁↔A₂ B₁↝B₂)
  where
  -- The first six clauses are included as optimisations intended to
  -- make some proof terms easier to work with. These clauses cover
  -- every possible use of B₁↝B₂′ in the expression above.

  B₁↝B₂′ :
     k₁ (A₁↔A₂ : A₁ ↔[ k₁ ] A₂) 
    (∀ x  B₁ x ↝[ k₂ ] B₂ (to-implication A₁↔A₂ x)) 
     k x 
    B₁ x ↝[ k₂ ] B₂ (to-implication {k = k} (from-isomorphism A₁↔A₂) x)
  B₁↝B₂′ bijection   _     B₁↝B₂ equivalence = B₁↝B₂
  B₁↝B₂′ bijection   _     B₁↝B₂ surjection  = B₁↝B₂
  B₁↝B₂′ equivalence _     B₁↝B₂ equivalence = B₁↝B₂
  B₁↝B₂′ equivalence _     B₁↝B₂ surjection  = B₁↝B₂
  B₁↝B₂′ k₁          A₁↔A₂ B₁↝B₂ k           = λ x 
    B₁ x                                                    ↝⟨ B₁↝B₂ x 
    B₂ (to-implication A₁↔A₂ x)                             ↝⟨ ≡⇒↝ _ $ cong  f  B₂ (f x)) $
                                                                 to-implication∘from-isomorphism k₁ k ⟩□
    B₂ (to-implication {k = k} (from-isomorphism A₁↔A₂) x)  

  A₁↝A₂ :  {k}  A₁ ↝[ k ] A₂
  A₁↝A₂ = from-isomorphism A₁↔A₂

  l₁ = lower-extensionality a₁ b₁
  l₂ = lower-extensionality a₂ b₂

  helper :
     k₂ 
    Extensionality? k₂ (a₁  a₂) (b₁  b₂) 
    (∀ k x  B₁ x ↝[ k₂ ]
             B₂ (to-implication {k = k} (from-isomorphism A₁↔A₂) x)) 
    ((x : A₁)  B₁ x) ↝[ k₂ ] ((x : A₂)  B₂ x)
  helper implication         _   = Π-cong-→          A₁↝A₂  (_$ surjection)
  helper logical-equivalence _   = Π-cong-⇔          A₁↝A₂  (_$ surjection)
  helper injection           ext = Π-cong-↣ (l₂ ext) A₁↝A₂  (_$ equivalence)
  helper embedding           ext = Π-cong-Emb ext    A₁↝A₂  (_$ equivalence)
  helper surjection          ext = Π-cong-↠ (l₁ ext) A₁↝A₂  (_$ surjection)
  helper bijection           ext = Π-cong-↔ ext      A₁↝A₂  (_$ equivalence)
  helper equivalence         ext = Π-cong-≃ ext      A₁↝A₂  (_$ equivalence)

-- A variant of Π-cong.

Π-cong-contra :
   {k₁ k₂ a₁ a₂ b₁ b₂} 
  Extensionality? k₂ (a₁  a₂) (b₁  b₂) 
  {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁  Set b₁} {B₂ : A₂  Set b₂} 
  (A₂↔A₁ : A₂ ↔[ k₁ ] A₁) 
  (∀ x  B₁ (to-implication A₂↔A₁ x) ↝[ k₂ ] B₂ x) 
  ((x : A₁)  B₁ x) ↝[ k₂ ] ((x : A₂)  B₂ x)
Π-cong-contra {k₁} {k₂} {a₁} {a₂} {b₁} {b₂}
              ext {A₁} {A₂} {B₁} {B₂} A₂↔A₁ B₁↝B₂ =
  helper k₂ ext (B₁↝B₂′ k₁ A₂↔A₁ B₁↝B₂)
  where
  -- The first six clauses are included as optimisations intended to
  -- make some proof terms easier to work with. These clauses cover
  -- every possible use of B₁↝B₂′ in the expression above.

  B₁↝B₂′ :
     k₁ (A₂↔A₁ : A₂ ↔[ k₁ ] A₁) 
    (∀ x  B₁ (to-implication A₂↔A₁ x) ↝[ k₂ ] B₂ x) 
     k x 
    B₁ (to-implication {k = k} (from-isomorphism A₂↔A₁) x) ↝[ k₂ ] B₂ x
  B₁↝B₂′ bijection   _     B₁↝B₂ equivalence = B₁↝B₂
  B₁↝B₂′ bijection   _     B₁↝B₂ implication = B₁↝B₂
  B₁↝B₂′ bijection   _     B₁↝B₂ surjection  = B₁↝B₂
  B₁↝B₂′ equivalence _     B₁↝B₂ equivalence = B₁↝B₂
  B₁↝B₂′ equivalence _     B₁↝B₂ implication = B₁↝B₂
  B₁↝B₂′ equivalence _     B₁↝B₂ surjection  = B₁↝B₂
  B₁↝B₂′ k₁          A₂↔A₁ B₁↝B₂ k           = λ x 
    B₁ (to-implication {k = k} (from-isomorphism A₂↔A₁) x)  ↝⟨ ≡⇒↝ _ $ cong  f  B₁ (f x)) $ sym $ to-implication∘from-isomorphism k₁ k 
    B₁ (to-implication A₂↔A₁ x)                             ↝⟨ B₁↝B₂ x ⟩□
    B₂ x                                                    

  A₂↝A₁ :  {k}  A₂ ↝[ k ] A₁
  A₂↝A₁ = from-isomorphism A₂↔A₁

  l₁ = lower-extensionality a₁ b₁
  l₂ = lower-extensionality a₂ b₂

  helper :
     k₂ 
    Extensionality? k₂ (a₁  a₂) (b₁  b₂) 
    (∀ k x  B₁ (to-implication {k = k} (from-isomorphism A₂↔A₁) x)
               ↝[ k₂ ]
             B₂ x) 
    ((x : A₁)  B₁ x) ↝[ k₂ ] ((x : A₂)  B₂ x)
  helper implication         _   = Π-cong-contra-→          A₂↝A₁  (_$ implication)
  helper logical-equivalence _   = Π-cong-contra-⇔          A₂↝A₁  (_$ surjection)
  helper injection           ext = Π-cong-contra-↣ (l₂ ext) A₂↝A₁  (_$ surjection)
  helper embedding           ext = Π-cong-contra-Emb ext    A₂↝A₁  (_$ equivalence)
  helper surjection          ext = Π-cong-contra-↠ (l₁ ext) A₂↝A₁  (_$ equivalence)
  helper bijection           ext = Π-cong-contra-↔ ext      A₂↝A₁  (_$ equivalence)
  helper equivalence         ext = Π-cong-contra-≃ ext      A₂↝A₁  (_$ equivalence)

Π-left-identity :  {a} {A :   Set a}  ((x : )  A x)  A tt
Π-left-identity = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f  f tt
      ; from = λ x _  x
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- A lemma that can be used to simplify a pi type where the domain is
-- isomorphic to the unit type.

drop-⊤-left-Π :
   {k a b} {A : Set a} {B : A  Set b} 
  Extensionality? k a b 
  (A↔⊤ : A  ) 
  ((x : A)  B x) ↝[ k ] B (_↔_.from A↔⊤ tt)
drop-⊤-left-Π {A = A} {B} ext A↔⊤ =
  ((x : A)  B x)                 ↝⟨ Π-cong-contra ext (inverse A↔⊤)  _  id) 
  ((x : )  B (_↔_.from A↔⊤ x))  ↔⟨ Π-left-identity ⟩□
  B (_↔_.from A↔⊤ tt)             

→-right-zero :  {a} {A : Set a}  (A  )  
→-right-zero = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ _  tt
      ; from = λ _ _  tt
      }
    ; right-inverse-of = λ _  refl tt
    }
  ; left-inverse-of = λ _  refl  _  tt)
  }

-- A lemma relating function types with the empty type as domain and
-- the unit type.

Π⊥↔⊤ :  {k  a} {A :  { = }  Set a} 
       Extensionality? k  a 
       ((x : )  A x) ↝[ k ] 
Π⊥↔⊤ = generalise-ext? Π⊥⇔⊤ λ ext  record
  { surjection = record
    { logical-equivalence = Π⊥⇔⊤
    ; right-inverse-of    = λ _  refl _
    }
  ; left-inverse-of = λ _  apply-ext ext  x  ⊥-elim x)
  }
  where
  Π⊥⇔⊤ = record
    { to   = _
    ; from = λ _ x  ⊥-elim x
    }

-- A lemma relating ¬ ⊥ and ⊤.

¬⊥↔⊤ :  {k } 
       Extensionality? k  lzero 
       ¬  { = } ↝[ k ] 
¬⊥↔⊤ = Π⊥↔⊤

-- Simplification lemmas for types of the form A → A → B.

→→↠→ :
   {a b} {A : Set a} {B : Set b} 
  (A  A  B)  (A  B)
→→↠→ = record
  { logical-equivalence = record
    { to   = λ f x  f x x
    ; from = λ f x _  f x
    }
  ; right-inverse-of = refl
  }

→→⊥↔→⊥ :
   {a } {A : Set a} 
  Extensionality a (a  ) 
  (A  A   { = })  (A   { = })
→→⊥↔→⊥ ext = record
  { surjection      = →→↠→
  ; left-inverse-of = λ f  apply-ext ext λ x  ⊥-elim (f x x)
  }

-- Π is "commutative".

Π-comm :  {a b c} {A : Set a} {B : Set b} {C : A  B  Set c} 
         (∀ x y  C x y)  (∀ y x  C x y)
Π-comm = record
  { surjection = record
    { logical-equivalence = record { to = flip; from = flip }
    ; right-inverse-of    = refl
    }
  ; left-inverse-of = refl
  }

-- Π and Σ commute (in a certain sense).

ΠΣ-comm :
   {a b c} {A : Set a} {B : A  Set b} {C : (x : A)  B x  Set c} 
  (∀ x   λ (y : B x)  C x y)
    
  ( λ (f :  x  B x)   x  C x (f x))
ΠΣ-comm = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f  proj₁  f , proj₂  f
      ; from = λ { (f , g) x  f x , g x }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- The implicit variant of Π and Σ commute (in a certain sense).

implicit-ΠΣ-comm :
   {a b c} {A : Set a} {B : A  Set b} {C : (x : A)  B x  Set c} 
  (∀ {x}   λ (y : B x)  C x y)
    
  ( λ (f :  {x}  B x)   {x}  C x f)
implicit-ΠΣ-comm {A = A} {B} {C} =
  (∀ {x}   λ (y : B x)  C x y)          ↝⟨ Bijection.implicit-Π↔Π 
  (∀ x   λ (y : B x)  C x y)            ↝⟨ ΠΣ-comm 
  ( λ (f :  x  B x)   x  C x (f x))  ↝⟨ inverse $ Σ-cong Bijection.implicit-Π↔Π  _  Bijection.implicit-Π↔Π) ⟩□
  ( λ (f :  {x}  B x)   {x}  C x f)  

-- A variant of extensionality-isomorphism for functions with implicit
-- arguments.

implicit-extensionality-isomorphism :
   {k a b} 
  Extensionality a b 
  {A : Set a} {B : A  Set b} {f g : {x : A}  B x} 
  (∀ x  f {x}  g {x}) ↔[ k ] ((λ {x}  f {x})  g)
implicit-extensionality-isomorphism ext {f = f} {g} =
  (∀ x  f {x}  g {x})            ↔⟨ Eq.extensionality-isomorphism ext 
  ((λ x  f {x})   x  g {x}))  ↔⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ (inverse Bijection.implicit-Π↔Π)) ⟩□
  ((λ {x}  f {x})  g)            

private

  -- The forward direction of
  -- implicit-extensionality-isomorphism {k = bijection} computes in a
  -- certain way.
  --
  -- Note that (at the time of writing) the proof below fails if the
  -- two occurrences of "inverse" in the previous proof are removed.

  to-implicit-extensionality-isomorphism :
     {a b}
    (ext : Extensionality a b) {A : Set a} {B : A  Set b}
    {f g : {x : A}  B x} (f≡g :  x  f {x}  g {x}) 
    _↔_.to (implicit-extensionality-isomorphism ext) f≡g
      
    implicit-extensionality (Eq.good-ext ext) f≡g
  to-implicit-extensionality-isomorphism _ _ = refl _

-- The Yoneda lemma, as given in the HoTT book, but specialised to the
-- opposite of the category of sets and functions, and with some
-- naturality properties omitted. (The proof uses extensionality.)

yoneda :
   {a b X} 
  Extensionality (lsuc a) (lsuc a  b) 
  (F : SET a  SET b) 
  (map :  {A B}  (Type A  Type B)  Type (F A)  Type (F B)) 
  (∀ {A} {x : Type (F A)}  map id x  x) 
  (∀ {A B C f g x} 
   (map {A = B} {B = C} f  map {A = A} g) x  map (f  g) x) 

  Type (F X)
    
   λ (γ :  Y  (Type X  Type Y)  Type (F Y)) 
     Y₁ Y₂ f g  map f (γ Y₁ g)  γ Y₂ (f  g)

yoneda {a} {X = X} ext F map map-id map-∘ = record
  { surjection = record
    { logical-equivalence = record
      { to = λ x   _ f  map f x) , λ _ _ f g 
          map f (map g x)  ≡⟨ map-∘ ⟩∎
          map (f  g) x    
      ; from = λ { (γ , _)  γ X id }
      }
    ; right-inverse-of = λ { (γ , h)  Σ-≡,≡→≡

        ((λ _ f  map f (γ X id))  ≡⟨ (apply-ext (lower-extensionality lzero (lsuc a) ext) λ Y 
                                       apply-ext (lower-extensionality _     (lsuc a) ext) λ f 
                                       h X Y f id) ⟩∎
          Y f  γ Y f)           )

        (_⇔_.to propositional⇔irrelevant
           (Π-closure                                      ext  1 λ _  
            Π-closure (lower-extensionality lzero (lsuc a) ext) 1 λ Y₂ 
            Π-closure (lower-extensionality _     (lsuc a) ext) 1 λ _  
            Π-closure (lower-extensionality _     (lsuc a) ext) 1 λ _  
            proj₂ (F Y₂) _ _)
           _ _) }
    }
  ; left-inverse-of = λ x 
      map id x  ≡⟨ map-id ⟩∎
      x         
  }

-- There is a (split) surjection from products of equality
-- isomorphisms to equalities.

Π≡↔≡-↠-≡ :  k {a} {A : Set a} (x y : A) 
           (∀ z  (z  x) ↔[ k ] (z  y))  (x  y)
Π≡↔≡-↠-≡ k x y = record
  { logical-equivalence = record { to = to; from = from }
  ; right-inverse-of    = to∘from
  }
  where
  to : (∀ z  (z  x) ↔[ k ] (z  y))  x  y
  to f = to-implication (f x) (refl x)

  from′ : x  y   z  (z  x)  (z  y)
  from′ x≡y z = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ z≡x  trans z≡x      x≡y
        ; from = λ z≡y  trans z≡y (sym x≡y)
        }
      ; right-inverse-of = λ z≡y  trans-[trans-sym]- z≡y x≡y
      }
    ; left-inverse-of = λ z≡x  trans-[trans]-sym z≡x x≡y
    }

  from : x  y   z  (z  x) ↔[ k ] (z  y)
  from x≡y z = from-bijection (from′ x≡y z)

  abstract
    to∘from :  x≡y  to (from x≡y)  x≡y
    to∘from x≡y =
      to (from x≡y)       ≡⟨ sym $ cong  f  f (refl x)) $ to-implication∘from-isomorphism bijection  k ⌋-iso 
      trans (refl x) x≡y  ≡⟨ trans-reflˡ _ ⟩∎
      x≡y                 

-- Products of equivalences of equalities are isomorphic to equalities
-- (assuming extensionality).

Π≡≃≡-↔-≡ :  {a}  Extensionality a a 
           {A : Set a} (x y : A) 
           (∀ z  (z  x)  (z  y))  (x  y)
Π≡≃≡-↔-≡ ext x y = record
  { surjection      = surj
  ; left-inverse-of = from∘to
  }
  where
  surj = Π≡↔≡-↠-≡ equivalence x y

  open _↠_ surj

  abstract
    from∘to :  f  from (to f)  f
    from∘to f =
      apply-ext ext λ z  Eq.lift-equality ext $ apply-ext ext λ z≡x 
        trans z≡x (_≃_.to (f x) (refl x))  ≡⟨ elim  {u v} u≡v 
                                                      (f :  z  (z  v)  (z  y)) 
                                                      trans u≡v (_≃_.to (f v) (refl v)) 
                                                      _≃_.to (f u) u≡v)
                                                    _ _  trans-reflˡ _)
                                                   z≡x f ⟩∎
        _≃_.to (f z) z≡x                   

-- One can introduce a universal quantifier by also introducing an
-- equality (perhaps assuming extensionality).

∀-intro :  {k a b} 
          Extensionality? k a (a  b) 
          {A : Set a} {x : A} (B : (y : A)  x  y  Set b) 
          B x (refl x) ↝[ k ] (∀ y (x≡y : x  y)  B