    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Basic lemmas showing that various types are related (isomorphic or
    -- equivalent or…)
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Function.Related.TypeIsomorphisms where

    open import Algebra.Bundles public
      using (Magma; Semigroup; Monoid; CommutativeMonoid; CommutativeSemiring)
    open import Algebra.Definitions
      using (Identity; LeftIdentity; RightIdentity; Zero; LeftZero; RightZero
            ; Associative; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_)
    open import Algebra.Structures public
      using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid
            ; IsCommutativeSemiring)
    open import Algebra.Structures.Biased using (isCommutativeSemiringˡ)
    open import Axiom.Extensionality.Propositional using (Extensionality)
    open import Data.Bool.Base using (true; false)
    open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
    open import Data.Product.Base as Product
      using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃; ∃-syntax)
    open import Data.Product.Function.NonDependent.Propositional
    open import Data.Sum.Base as Sum
    open import Data.Sum.Properties using (swap-involutive)
    open import Data.Sum.Function.Propositional using (_⊎-cong_)
    open import Data.Unit.Polymorphic.Base using (⊤)
    open import Level using (Level; Lift; 0ℓ; suc)
    open import Function.Base
    open import Function.Bundles
    open import Function.Related.Propositional
    import Function.Construct.Identity as Identity
    open import Relation.Binary hiding (_⇔_)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
    open import Relation.Binary.PropositionalEquality.Properties
      using (module ≡-Reasoning)
    open import Relation.Nullary.Negation.Core using (¬_)
    import Relation.Nullary.Indexed as I

    private
      variable
        a b c d : Level
        A B C D : Set a

    ------------------------------------------------------------------------
    -- A lemma relating True dec and P, where dec : Dec P

    open import Relation.Nullary.Decidable public
      using ()
      renaming (True-↔ to True↔)

    ------------------------------------------------------------------------
    -- Properties of Σ and _×_

    -- Σ is associative
    Σ-assoc : ∀ {A : Set a} {B : A → Set b} {C : (a : A) → B a → Set c} →
              Σ (Σ A B) (uncurry C) ↔ Σ A (λ a → Σ (B a) (C a))
    Σ-assoc = mk↔ₛ′ Product.assocʳ Product.assocˡ (λ _ → refl) (λ _ → refl)

    -- × is commutative

    ×-comm : ∀ (A : Set a) (B : Set b) → (A × B) ↔ (B × A)
    ×-comm _ _ = mk↔ₛ′ Product.swap Product.swap (λ _ → refl) λ _ → refl

    -- × has ⊤ as its identity

    ×-identityˡ : ∀ ℓ → LeftIdentity  {ℓ = ℓ} _↔_ ⊤ _×_
    ×-identityˡ _ _ = mk↔ₛ′ proj₂ -,_ (λ _ → refl) (λ _ → refl)

    ×-identityʳ : ∀ ℓ → RightIdentity  {ℓ = ℓ} _↔_ ⊤ _×_
    ×-identityʳ _ _ = mk↔ₛ′ proj₁ (_, _) (λ _ → refl) (λ _ → refl)

    ×-identity : ∀ ℓ → Identity _↔_ ⊤ _×_
    ×-identity ℓ = ×-identityˡ ℓ , ×-identityʳ ℓ

    -- × has ⊥ has its zero

    ×-zeroˡ : ∀ ℓ → LeftZero {ℓ = ℓ} _↔_ ⊥ _×_
    ×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥-elim > (λ _ → refl) (λ { () })

    ×-zeroʳ : ∀ ℓ → RightZero {ℓ = ℓ} _↔_ ⊥ _×_
    ×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥-elim , id > (λ _ → refl) (λ { () })

    ×-zero : ∀ ℓ → Zero _↔_ ⊥ _×_
    ×-zero ℓ  = ×-zeroˡ ℓ , ×-zeroʳ ℓ

    ------------------------------------------------------------------------
    -- Properties of ⊎

    -- ⊎ is associative

    ⊎-assoc : ∀ ℓ → Associative {ℓ = ℓ} _↔_ _⊎_
    ⊎-assoc ℓ _ _ _ = mk↔ₛ′
      [ [ inj₁ , inj₂ ∘′ inj₁ ]′ , inj₂ ∘′ inj₂ ]′
      [ inj₁ ∘′ inj₁ , [ inj₁ ∘′ inj₂ , inj₂ ]′ ]′
      [ (λ _ → refl) , [ (λ _ → refl) , (λ _ → refl) ] ]
      [ [ (λ _ → refl) , (λ _ → refl) ] , (λ _ → refl) ]

    -- ⊎ is commutative

    ⊎-comm : ∀ (A : Set a) (B : Set b) → (A ⊎ B) ↔ (B ⊎ A)
    ⊎-comm _ _ = mk↔ₛ′ swap swap swap-involutive swap-involutive

    -- ⊎ has ⊥ as its identity

    ⊎-identityˡ : ∀ ℓ → LeftIdentity _↔_ (⊥ {ℓ}) _⊎_
    ⊎-identityˡ _ _ = mk↔ₛ′ [ (λ ()) , id ]′ inj₂ (λ _ → refl)
                              [ (λ ()) , (λ _ → refl) ]

    ⊎-identityʳ : ∀ ℓ → RightIdentity _↔_ (⊥ {ℓ}) _⊎_
    ⊎-identityʳ _ _ = mk↔ₛ′ [ id , (λ ()) ]′ inj₁ (λ _ → refl)
                              [ (λ _ → refl) , (λ ()) ]

    ⊎-identity : ∀ ℓ → Identity _↔_ ⊥ _⊎_
    ⊎-identity ℓ = ⊎-identityˡ ℓ , ⊎-identityʳ ℓ

    ------------------------------------------------------------------------
    -- Properties of Σ and ⊎

    -- Σ distributes over ⊎

    Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} →
      (∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q)
    Σ-distribˡ-⊎ = mk↔ₛ′
      (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
      [ Product.map₂ inj₁ , Product.map₂ inj₂ ]′
      [ (λ _ → refl) , (λ _ → refl) ]
      (uncurry λ _ → [ (λ _ → refl) , (λ _ → refl) ])

    Σ-distribʳ-⊎ : {P : A ⊎ B → Set c} →
      (Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂))
    Σ-distribʳ-⊎ = mk↔ₛ′
      (uncurry [ curry inj₁ , curry inj₂ ])
      [ Product.dmap inj₁ id , Product.dmap inj₂ id ]
      [ (λ _ → refl) , (λ _ → refl) ]
      (uncurry [ (λ _ _ → refl) , (λ _ _ → refl) ])

    ------------------------------------------------------------------------
    -- Properties of × and ⊎

    -- × distributes over ⊎
    -- primed variants are less level polymorphic

    ×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
    ×-distribˡ-⊎ = Σ-distribˡ-⊎

    ×-distribˡ-⊎′ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_
    ×-distribˡ-⊎′ ℓ _ _ _ = ×-distribˡ-⊎

    ×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C)
    ×-distribʳ-⊎ = Σ-distribʳ-⊎

    ×-distribʳ-⊎′ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_
    ×-distribʳ-⊎′ ℓ _ _ _ = ×-distribʳ-⊎

    ×-distrib-⊎′ : ∀ ℓ → _DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_
    ×-distrib-⊎′ ℓ = ×-distribˡ-⊎′ ℓ , ×-distribʳ-⊎′ ℓ

    ------------------------------------------------------------------------
    -- ⊥, ⊤, _×_ and _⊎_ form a commutative semiring

    -- ⊤, _×_ form a commutative monoid

    ×-isMagma : ∀ k ℓ → IsMagma {Level.suc ℓ} (Related ⌊ k ⌋) _×_
    ×-isMagma k ℓ = record
      { isEquivalence = SK-isEquivalence k
      ; ∙-cong        = _×-cong_
      }

    ×-magma : SymmetricKind → (ℓ : Level) → Magma _ _
    ×-magma k ℓ = record
      { isMagma = ×-isMagma k ℓ
      }

    ×-isSemigroup : ∀ k ℓ → IsSemigroup {Level.suc ℓ} (Related ⌊ k ⌋) _×_
    ×-isSemigroup k ℓ = record
      { isMagma = ×-isMagma k ℓ
      ; assoc   = λ _ _ _ → ↔⇒ Σ-assoc
      }

    ×-semigroup : SymmetricKind → (ℓ : Level) → Semigroup _ _
    ×-semigroup k ℓ = record
      { isSemigroup = ×-isSemigroup k ℓ
      }

    ×-isMonoid : ∀ k ℓ → IsMonoid (Related ⌊ k ⌋) _×_ ⊤
    ×-isMonoid k ℓ = record
      { isSemigroup = ×-isSemigroup k ℓ
      ; identity    = (↔⇒ ∘ ×-identityˡ ℓ) , (↔⇒ ∘ ×-identityʳ ℓ)
      }

    ×-monoid : SymmetricKind → (ℓ : Level) → Monoid _ _
    ×-monoid k ℓ = record
      { isMonoid = ×-isMonoid k ℓ
      }

    ×-isCommutativeMonoid : ∀ k ℓ → IsCommutativeMonoid (Related ⌊ k ⌋) _×_ ⊤
    ×-isCommutativeMonoid k ℓ = record
      { isMonoid = ×-isMonoid k ℓ
      ; comm     = λ _ _ → ↔⇒ (×-comm _ _)
      }

    ×-commutativeMonoid : SymmetricKind → (ℓ : Level) → CommutativeMonoid _ _
    ×-commutativeMonoid k ℓ = record
      { isCommutativeMonoid = ×-isCommutativeMonoid k ℓ
      }

    -- ⊥, _⊎_ form a commutative monoid

    ⊎-isMagma : ∀ k ℓ → IsMagma {Level.suc ℓ} (Related ⌊ k ⌋) _⊎_
    ⊎-isMagma k ℓ = record
      { isEquivalence = SK-isEquivalence k
      ; ∙-cong        = _⊎-cong_
      }

    ⊎-magma : SymmetricKind → (ℓ : Level) → Magma _ _
    ⊎-magma k ℓ = record
      { isMagma = ⊎-isMagma k ℓ
      }

    ⊎-isSemigroup : ∀ k ℓ → IsSemigroup {Level.suc ℓ} (Related ⌊ k ⌋) _⊎_
    ⊎-isSemigroup k ℓ = record
      { isMagma = ⊎-isMagma k ℓ
      ; assoc   = λ A B C → ↔⇒ (⊎-assoc ℓ A B C)
      }

    ⊎-semigroup : SymmetricKind → (ℓ : Level) → Semigroup _ _
    ⊎-semigroup k ℓ = record
      { isSemigroup = ⊎-isSemigroup k ℓ
      }

    ⊎-isMonoid : ∀ k ℓ → IsMonoid (Related ⌊ k ⌋) _⊎_ ⊥
    ⊎-isMonoid k ℓ = record
      { isSemigroup = ⊎-isSemigroup k ℓ
      ; identity    = (↔⇒ ∘ ⊎-identityˡ ℓ) , (↔⇒ ∘ ⊎-identityʳ ℓ)
      }

    ⊎-monoid : SymmetricKind → (ℓ : Level) → Monoid _ _
    ⊎-monoid k ℓ = record
      { isMonoid = ⊎-isMonoid k ℓ
      }

    ⊎-isCommutativeMonoid : ∀ k ℓ → IsCommutativeMonoid (Related ⌊ k ⌋) _⊎_ ⊥
    ⊎-isCommutativeMonoid k ℓ = record
      { isMonoid = ⊎-isMonoid k ℓ
      ; comm     = λ _ _ → ↔⇒ (⊎-comm _ _)
      }

    ⊎-commutativeMonoid : SymmetricKind → (ℓ : Level) →
                          CommutativeMonoid _ _
    ⊎-commutativeMonoid k ℓ = record
      { isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ
      }

    ×-⊎-isCommutativeSemiring : ∀ k ℓ →
      IsCommutativeSemiring (Related ⌊ k ⌋) _⊎_ _×_ ⊥ ⊤
    ×-⊎-isCommutativeSemiring k ℓ = isCommutativeSemiringˡ record
      { +-isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ
      ; *-isCommutativeMonoid = ×-isCommutativeMonoid k ℓ
      ; distribʳ              = λ _ _ _ → ↔⇒ ×-distribʳ-⊎
      ; zeroˡ                 = ↔⇒ ∘ ×-zeroˡ ℓ
      }

    ×-⊎-commutativeSemiring : SymmetricKind → (ℓ : Level) →
                              CommutativeSemiring (Level.suc ℓ) ℓ
    ×-⊎-commutativeSemiring k ℓ = record
      { isCommutativeSemiring = ×-⊎-isCommutativeSemiring k ℓ
      }

    ------------------------------------------------------------------------
    -- Some reordering lemmas

    ΠΠ↔ΠΠ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
            ((x : A) (y : B) → P x y) ↔ ((y : B) (x : A) → P x y)
    ΠΠ↔ΠΠ _ = mk↔ₛ′ flip flip (λ _ → refl) (λ _ → refl)

    ∃∃↔∃∃ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
            (∃₂ λ x y → P x y) ↔ (∃₂ λ y x → P x y)
    ∃∃↔∃∃ P = mk↔ₛ′ to from (λ _ → refl) (λ _ → refl)
      where
      to : (∃₂ λ x y → P x y) → (∃₂ λ y x → P x y)
      to (x , y , Pxy) = (y , x , Pxy)

      from : (∃₂ λ y x → P x y) → (∃₂ λ x y → P x y)
      from (y , x , Pxy) = (x , y , Pxy)

    ------------------------------------------------------------------------
    -- Implicit and explicit function spaces are isomorphic

    Π↔Π : ∀ {A : Set a} {B : A → Set b} →
          ((x : A) → B x) ↔ ({x : A} → B x)
    Π↔Π = mk↔ₛ′ _$- λ- (λ _ → refl) (λ _ → refl)

    ------------------------------------------------------------------------
    -- _→_ preserves the symmetric relations

    →-cong-⇔ : A ⇔ B → C ⇔ D → (A → C) ⇔ (B → D)
    →-cong-⇔ A⇔B C⇔D = mk⇔
      (λ f → to C⇔D ∘ f ∘ from A⇔B)
      (λ f → from C⇔D ∘ f ∘ to A⇔B)
      where open Equivalence

    →-cong-↔ : Extensionality a c → Extensionality b d →
                 {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
                 A ↔ B → C ↔ D → (A → C) ↔ (B → D)
    →-cong-↔ ext₁ ext₂ A↔B C↔D = mk↔ₛ′
      (λ f → to C↔D ∘ f ∘ from A↔B)
      (λ f → from C↔D ∘ f ∘ to A↔B)
      (λ f → ext₂ λ x → begin
        to C↔D (from C↔D (f (to A↔B (from A↔B x)))) ≡⟨ strictlyInverseˡ C↔D _ ⟩
        f (to A↔B (from A↔B x))                     ≡⟨ cong f $ strictlyInverseˡ A↔B x ⟩
        f x                                         ∎)
      (λ f → ext₁ λ x → begin
        from C↔D (to C↔D (f (from A↔B (to A↔B x)))) ≡⟨ strictlyInverseʳ C↔D _ ⟩
        f (from A↔B (to A↔B x))                     ≡⟨ cong f $ strictlyInverseʳ A↔B x ⟩
        f x                                         ∎)
      where open Inverse; open ≡-Reasoning

    →-cong :  Extensionality a c → Extensionality b d →
              ∀ {k} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
              A ∼[ ⌊ k ⌋ ] B → C ∼[ ⌊ k ⌋ ] D → (A → C) ∼[ ⌊ k ⌋ ] (B → D)
    →-cong extAC extBD {equivalence} = →-cong-⇔
    →-cong extAC extBD {bijection}   = →-cong-↔ extAC extBD

    ------------------------------------------------------------------------
    -- ¬_ (at Level 0) preserves the symmetric relations

    ¬-cong-⇔ : A ⇔ B → (¬ A) ⇔ (¬ B)
    ¬-cong-⇔ A⇔B = →-cong-⇔ A⇔B (Identity.⇔-id _)

    ¬-cong : Extensionality a 0ℓ → Extensionality b 0ℓ →
             ∀ {k} {A : Set a} {B : Set b} →
             A ∼[ ⌊ k ⌋ ] B → (¬ A) ∼[ ⌊ k ⌋ ] (¬ B)
    ¬-cong extA extB A≈B = →-cong extA extB A≈B (K-reflexive refl)

    ------------------------------------------------------------------------
    -- _⇔_ preserves _⇔_

    -- The type of the following proof is a bit more general.

    Related-cong :
      ∀ {k} →
      A ∼[ ⌊ k ⌋ ] B → C ∼[ ⌊ k ⌋ ] D → (A ∼[ ⌊ k ⌋ ] C) ⇔ (B ∼[ ⌊ k ⌋ ] D)
    Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
      (λ A≈C → B  ∼⟨ SK-sym A≈B ⟩
                A  ∼⟨ A≈C ⟩
                C  ∼⟨ C≈D ⟩
                D  ∎)
      (λ B≈D → A  ∼⟨ A≈B ⟩
                B  ∼⟨ B≈D ⟩
                D  ∼⟨ SK-sym C≈D ⟩
                C  ∎)
      where open EquationalReasoning

    ------------------------------------------------------------------------
    -- Relating a predicate to an existentially quantified one with the
    -- restriction that the quantified variable is equal to the given one

    ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
    ∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py)
      (λ where (_ , refl , _) → refl) (λ where _ → refl)