```------------------------------------------------------------------------
-- 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 _≃_; Is-equivalence)
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 (_↠_; Split-surjective)

------------------------------------------------------------------------
-- 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} â b̂ →
Extensionality? k (a ⊔ â) (b ⊔ b̂) → Extensionality? k a b
lower-extensionality? k with extensionality? k
... | without-extensionality _ = _
... | with-extensionality    _ = lower-extensionality

-- Some functions that can be used to generalise results.

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

generalise-ext?-prop :
∀ {k a b c d} {A : Set a} {B : Set b} →
A ⇔ B →
(Extensionality c d → Is-proposition A) →
(Extensionality c d → Is-proposition B) →
Extensionality? k c d → A ↝[ k ] B
generalise-ext?-prop f⇔ A-prop B-prop =
generalise-ext?
f⇔
(λ ext → _≃_.bijection \$
_↠_.from (Eq.≃↠⇔ (A-prop ext) (B-prop ext)) f⇔)

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

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

inverse-ext? :
∀ {k a b c d} {A : Set a} {B : Set b} →
(∀ {k} → Extensionality? k c d → A ↝[ k ] B) →
Extensionality? k c d → B ↝[ k ] A
inverse-ext? hyp = generalise-ext?-sym (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 ≡⇒↝ in terms of subst.

≡⇒↝-in-terms-of-subst :
∀ k {ℓ} {A B : Set ℓ} (A≡B : A ≡ B) →
≡⇒↝ k A≡B ≡ subst (A ↝[ k ]_) A≡B id
≡⇒↝-in-terms-of-subst k {B = B} = elim₁
(λ {A} A≡B → ≡⇒↝ k A≡B ≡ subst (A ↝[ k ]_) A≡B id)
(≡⇒↝ k (refl B)                 ≡⟨ ≡⇒↝-refl ⟩
id                             ≡⟨ sym \$ subst-refl _ _ ⟩∎
subst (B ↝[ k ]_) (refl B) id  ∎)

≡⇒↝-in-terms-of-subst-sym :
∀ k {ℓ} {A B : Set ℓ} (A≡B : A ≡ B) →
≡⇒↝ k A≡B ≡ subst (_↝[ k ] B) (sym A≡B) id
≡⇒↝-in-terms-of-subst-sym k {B = B} = elim₁
(λ {A} A≡B → ≡⇒↝ k A≡B ≡ subst (_↝[ k ] B) (sym A≡B) id)
(≡⇒↝ k (refl B)                       ≡⟨ ≡⇒↝-refl ⟩
id                                   ≡⟨ sym \$ subst-refl _ _ ⟩
subst (_↝[ k ] B) (refl B) id        ≡⟨ cong (flip (subst _) _) \$ sym sym-refl ⟩∎
subst (_↝[ k ] B) (sym (refl B)) id  ∎)

-- 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₁ : ∀ {x₁ y₁} (_ : x₁ ≡ y₁) → _
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 Σ/∃/_×_

-- Σ preserves isomorphisms in its first argument and all kinds of
-- functions in its second argument.

Σ-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} {implication}         = Eq.∃-preserves-functions            ⊚ from-isomorphism
Σ-cong {equivalence} {logical-equivalence} = Eq.∃-preserves-logical-equivalences ⊚ from-isomorphism
Σ-cong {equivalence} {injection}           = Eq.∃-preserves-injections
Σ-cong {equivalence} {embedding}           = Σ-preserves-embeddings              ⊚ from-isomorphism
Σ-cong {equivalence} {surjection}          = Eq.∃-preserves-surjections          ⊚ from-isomorphism
Σ-cong {equivalence} {bijection}           = Eq.∃-preserves-bijections
Σ-cong {equivalence} {equivalence}         = Eq.Σ-preserves
Σ-cong {bijection}   {implication}         = Eq.∃-preserves-functions            ⊚ from-isomorphism
Σ-cong {bijection}   {logical-equivalence} = Eq.∃-preserves-logical-equivalences ⊚ from-isomorphism
Σ-cong {bijection}   {injection}           = Eq.∃-preserves-injections           ⊚ from-isomorphism
Σ-cong {bijection}   {embedding}           = Σ-preserves-embeddings              ⊚ from-isomorphism
Σ-cong {bijection}   {surjection}          = Eq.∃-preserves-surjections          ⊚ from-isomorphism
Σ-cong {bijection}   {bijection}           = Eq.∃-preserves-bijections           ⊚ from-isomorphism
Σ-cong {bijection}   {equivalence}         = Eq.Σ-preserves                      ⊚ from-isomorphism

-- A variant of Σ-cong.

Σ-cong-contra :
∀ {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₁ (to-implication A₂↔A₁ x) ↝[ k₂ ] B₂ x) →
Σ A₁ B₁ ↝[ k₂ ] Σ A₂ B₂
Σ-cong-contra {k₁} {k₂} {A₁ = A₁} {A₂} {B₁} {B₂} A₂↔A₁ B₁↝B₂ =
Σ-cong A₁↔A₂ B₁↝B₂′
where
A₁↔A₂ : A₁ ↔ A₂
A₁↔A₂ = inverse \$ from-isomorphism A₂↔A₁

B₁↝B₂′ : ∀ x → B₁ x ↝[ k₂ ] B₂ (_↔_.to A₁↔A₂ x)
B₁↝B₂′ x =
B₁ x                                        ↝⟨ ≡⇒↝ _ \$ cong B₁ \$ sym \$ _↔_.left-inverse-of A₁↔A₂ _ ⟩
B₁ (_↔_.from A₁↔A₂ (_↔_.to A₁↔A₂ x))        ↝⟨ ≡⇒↝ _ \$ cong (λ f → B₁ (f (_↔_.to A₁↔A₂ x))) \$ sym \$
to-implication∘from-isomorphism k₁ bijection ⟩
B₁ (to-implication A₂↔A₁ (_↔_.to A₁↔A₂ x))  ↝⟨ B₁↝B₂ (_↔_.to A₁↔A₂ x) ⟩□
B₂ (_↔_.to A₁↔A₂ x)                         □

-- Variants of special cases of Σ-cong-contra.

Σ-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) →
Σ A₁ B₁ → Σ A₂ B₂
Σ-cong-contra-→ {B₁ = B₁} A₂↠A₁ B₁→B₂ =
Σ-map (_↠_.from A₂↠A₁)
(B₁→B₂ _ ∘ subst B₁ (sym \$ _↠_.right-inverse-of A₂↠A₁ _))

Σ-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) →
Σ A₁ B₁ ⇔ Σ A₂ B₂
Σ-cong-contra-⇔ A₂↠A₁ B₁⇔B₂ =
inverse \$
Eq.∃-preserves-logical-equivalences A₂↠A₁ (inverse ⊚ B₁⇔B₂)

-- ∃ 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⇔↔⊤ \$
⇒≡ 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 relating equality of certain kinds of functions to
-- pointwise equality of the underlying functions

-- 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 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 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 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                                                  □

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

Embedding-to-≡↔≡ :
∀ {a b} →
Extensionality (a ⊔ b) (a ⊔ b) →
{A : Set a} {B : Set b} {p q : Embedding A B} →
(∀ x → Embedding.to p x ≡ Embedding.to q x) ↔ p ≡ q
Embedding-to-≡↔≡ {a} {b} ext {p = p} {q} =
(∀ x → Embedding.to p x ≡ Embedding.to q x)    ↔⟨ Eq.extensionality-isomorphism (lower-extensionality b a ext) ⟩

Embedding.to p ≡ Embedding.to q                ↝⟨ ignore-propositional-component (Emb.Is-embedding-propositional ext) ⟩

(Embedding.to p , Embedding.is-embedding p) ≡
(Embedding.to q , Embedding.is-embedding q)    ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ Emb.Embedding-as-Σ) ⟩□

p ≡ q                                          □

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

-- 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 = λ _ → 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) ⟩□
⊥  □
})

-- Is-equivalence preserves equality, if we see _≃_ as a form of
-- equality (assuming extensionality).

Is-equivalence-cong :
∀ {k a b} {A : Set a} {B : Set b} {f g : A → B} →
Extensionality? k (a ⊔ b) (a ⊔ b) →
(∀ x → f x ≡ g x) →
Is-equivalence f ↝[ k ] Is-equivalence g
Is-equivalence-cong ext f≡g =
generalise-ext?-prop
(record
{ to   = Eq.respects-extensional-equality f≡g
; from = Eq.respects-extensional-equality (sym ⊚ f≡g)
})
(λ ext → Eq.propositional ext _)
(λ ext → Eq.propositional ext _)
ext

-- _≃_ is commutative (assuming extensionality).

≃-comm :
∀ {k a b} {A : Set a} {B : Set b} →
Extensionality? k (a ⊔ b) (a ⊔ b) →
A ≃ B ↝[ k ] B ≃ A
≃-comm =
generalise-ext?
Eq.inverse-logical-equivalence
Eq.inverse-isomorphism

------------------------------------------------------------------------
-- _⊎_ 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

-- A variant of →-cong.

→-cong₁ :
∀ {k₁ k₂ a b c} →
Extensionality? k₂ (a ⊔ b) c →
{A : Set a} {B : Set b} {C : Set c} →
A ↔[ k₁ ] B → (A → C) ↝[ k₂ ] (B → C)
→-cong₁ ext hyp = generalise-ext?-sym
(λ ext → →-cong ext (from-bijection (from-isomorphism hyp)) id)
ext

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)))          ≡⟨ dcong 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 (_↠_.from (B₁↠B₂ _) (f _)))) \$ 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)) \$
dcong (λ 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)

-- A variant of Π-cong for implicit Πs.

implicit-Π-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)
implicit-Π-cong ext {A₁} {A₂} {B₁} {B₂} A₁↔A₂ B₁↝B₂ =
({x : A₁} → B₁ x)  ↔⟨ Bijection.implicit-Π↔Π ⟩
((x : A₁) → B₁ x)  ↝⟨ Π-cong ext A₁↔A₂ B₁↝B₂ ⟩
((x : A₂) → B₂ x)  ↔⟨ inverse Bijection.implicit-Π↔Π ⟩□
({x : A₂} → B₂ x)  □

-- A variant of Π-cong-contra for implicit Πs.

implicit-Π-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)
implicit-Π-cong-contra ext {A₁} {A₂} {B₁} {B₂} A₁↔A₂ B₁↝B₂ =
({x : A₁} → B₁ x)  ↔⟨ Bijection.implicit-Π↔Π ⟩
((x : A₁) → B₁ x)  ↝⟨ Π-cong-contra ext A₁↔A₂ B₁↝B₂ ⟩
((x : A₂) → B₂ x)  ↔⟨ inverse Bijection.implicit-Π↔Π ⟩□
({x : A₂} → B₂ x)  □

Π-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 = λ _ ```