------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums of binary relations
------------------------------------------------------------------------

module Relation.Binary.Sum where

open import Data.Sum as Sum
open import Data.Product
open import Data.Unit using (⊤)
open import Data.Empty
open import Function
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
  using (Injection; _↣_; module Injection)
open import Function.Inverse as Inv
  using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (LeftInverse; _↞_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} where

  ----------------------------------------------------------------------
  -- Sums of relations

  infixr 1 _⊎-Rel_ _⊎-<_

  -- Generalised sum.

  data ⊎ʳ {ℓ₁ ℓ₂} (P : Set) (_∼₁_ : Rel A₁ ℓ₁) (_∼₂_ : Rel A₂ ℓ₂) :
          A₁ ⊎ A₂ → A₁ ⊎ A₂ → Set (a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂) where
    ₁∼₂ : ∀ {x y} (p : P)         → ⊎ʳ P _∼₁_ _∼₂_ (inj₁ x) (inj₂ y)
    ₁∼₁ : ∀ {x y} (x∼₁y : x ∼₁ y) → ⊎ʳ P _∼₁_ _∼₂_ (inj₁ x) (inj₁ y)
    ₂∼₂ : ∀ {x y} (x∼₂y : x ∼₂ y) → ⊎ʳ P _∼₁_ _∼₂_ (inj₂ x) (inj₂ y)

  -- Pointwise sum.

  _⊎-Rel_ : ∀ {ℓ₁ ℓ₂} → Rel A₁ ℓ₁ → Rel A₂ ℓ₂ → Rel (A₁ ⊎ A₂) _
  _⊎-Rel_ = ⊎ʳ ⊥

  -- All things to the left are "smaller than" all things to the
  -- right.

  _⊎-<_ : ∀ {ℓ₁ ℓ₂} → Rel A₁ ℓ₁ → Rel A₂ ℓ₂ → Rel (A₁ ⊎ A₂) _
  _⊎-<_ = ⊎ʳ ⊤

  ----------------------------------------------------------------------
  -- Helpers

  private

    ₁≁₂ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
          ∀ {x y} → ¬ (inj₁ x ⟨ ∼₁ ⊎-Rel ∼₂ ⟩ inj₂ y)
    ₁≁₂ (₁∼₂ ())

    drop-inj₁ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                ∀ {P x y} → inj₁ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩ inj₁ y → ∼₁ x y
    drop-inj₁ (₁∼₁ x∼y) = x∼y

    drop-inj₂ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                ∀ {P x y} → inj₂ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩ inj₂ y → ∼₂ x y
    drop-inj₂ (₂∼₂ x∼y) = x∼y

  ----------------------------------------------------------------------
  -- Some properties which are preserved by the relation formers above

  _⊎-reflexive_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₁′}
                    {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {∼₂ : Rel A₂ ℓ₂′} →
                  ≈₁ ⇒ ∼₁ → ≈₂ ⇒ ∼₂ →
                  ∀ {P} → (≈₁ ⊎-Rel ≈₂) ⇒ (⊎ʳ P ∼₁ ∼₂)
  refl₁ ⊎-reflexive refl₂ = refl
    where
    refl : (_ ⊎-Rel _) ⇒ (⊎ʳ _ _ _)
    refl (₁∼₁ x₁≈y₁) = ₁∼₁ (refl₁ x₁≈y₁)
    refl (₂∼₂ x₂≈y₂) = ₂∼₂ (refl₂ x₂≈y₂)
    refl (₁∼₂ ())

  _⊎-refl_ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
             Reflexive ∼₁ → Reflexive ∼₂ → Reflexive (∼₁ ⊎-Rel ∼₂)
  refl₁ ⊎-refl refl₂ = refl
    where
    refl : Reflexive (_ ⊎-Rel _)
    refl {x = inj₁ _} = ₁∼₁ refl₁
    refl {x = inj₂ _} = ₂∼₂ refl₂

  _⊎-irreflexive_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
                      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
                    Irreflexive ≈₁ <₁ → Irreflexive ≈₂ <₂ →
                    ∀ {P} → Irreflexive (≈₁ ⊎-Rel ≈₂) (⊎ʳ P <₁ <₂)
  irrefl₁ ⊎-irreflexive irrefl₂ = irrefl
    where
    irrefl : Irreflexive (_ ⊎-Rel _) (⊎ʳ _ _ _)
    irrefl (₁∼₁ x₁≈y₁) (₁∼₁ x₁<y₁) = irrefl₁ x₁≈y₁ x₁<y₁
    irrefl (₂∼₂ x₂≈y₂) (₂∼₂ x₂<y₂) = irrefl₂ x₂≈y₂ x₂<y₂
    irrefl (₁∼₂ ())    _

  _⊎-symmetric_ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                  Symmetric ∼₁ → Symmetric ∼₂ → Symmetric (∼₁ ⊎-Rel ∼₂)
  sym₁ ⊎-symmetric sym₂ = sym
    where
    sym : Symmetric (_ ⊎-Rel _)
    sym (₁∼₁ x₁∼y₁) = ₁∼₁ (sym₁ x₁∼y₁)
    sym (₂∼₂ x₂∼y₂) = ₂∼₂ (sym₂ x₂∼y₂)
    sym (₁∼₂ ())

  _⊎-transitive_ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                   Transitive ∼₁ → Transitive ∼₂ →
                   ∀ {P} → Transitive (⊎ʳ P ∼₁ ∼₂)
  trans₁ ⊎-transitive trans₂ = trans
    where
    trans : Transitive (⊎ʳ _ _ _)
    trans (₁∼₁ x∼y) (₁∼₁ y∼z) = ₁∼₁ (trans₁ x∼y y∼z)
    trans (₂∼₂ x∼y) (₂∼₂ y∼z) = ₂∼₂ (trans₂ x∼y y∼z)
    trans (₁∼₂ p)   (₂∼₂ _)     = ₁∼₂ p
    trans (₁∼₁ _)   (₁∼₂ p)     = ₁∼₂ p

  _⊎-antisymmetric_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
                        {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
                      Antisymmetric ≈₁ ≤₁ → Antisymmetric ≈₂ ≤₂ →
                      ∀ {P} → Antisymmetric (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ≤₁ ≤₂)
  antisym₁ ⊎-antisymmetric antisym₂ = antisym
    where
    antisym : Antisymmetric (_ ⊎-Rel _) (⊎ʳ _ _ _)
    antisym (₁∼₁ x≤y) (₁∼₁ y≤x) = ₁∼₁ (antisym₁ x≤y y≤x)
    antisym (₂∼₂ x≤y) (₂∼₂ y≤x) = ₂∼₂ (antisym₂ x≤y y≤x)
    antisym (₁∼₂ _)   ()

  _⊎-asymmetric_ : ∀ {ℓ₁ ℓ₂} {<₁ : Rel A₁ ℓ₁} {<₂ : Rel A₂ ℓ₂} →
                   Asymmetric <₁ → Asymmetric <₂ →
                   ∀ {P} → Asymmetric (⊎ʳ P <₁ <₂)
  asym₁ ⊎-asymmetric asym₂ = asym
    where
    asym : Asymmetric (⊎ʳ _ _ _)
    asym (₁∼₁ x<y) (₁∼₁ y<x) = asym₁ x<y y<x
    asym (₂∼₂ x<y) (₂∼₂ y<x) = asym₂ x<y y<x
    asym (₁∼₂ _)   ()

  _⊎-≈-respects₂_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₁′}
                      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {∼₂ : Rel A₂ ℓ₂′} →
                    ∼₁ Respects₂ ≈₁ → ∼₂ Respects₂ ≈₂ →
                    ∀ {P} → (⊎ʳ P ∼₁ ∼₂) Respects₂ (≈₁ ⊎-Rel ≈₂)
  _⊎-≈-respects₂_ {≈₁ = ≈₁} {∼₁ = ∼₁}{≈₂ = ≈₂} {∼₂ = ∼₂}
                  resp₁ resp₂ {P} =
    (λ {_ _ _} → resp¹) ,
    (λ {_ _ _} → resp²)
    where
    resp¹ : ∀ {x} → ((⊎ʳ P ∼₁ ∼₂) x) Respects (≈₁ ⊎-Rel ≈₂)
    resp¹ (₁∼₁ y≈y') (₁∼₁ x∼y) = ₁∼₁ (proj₁ resp₁ y≈y' x∼y)
    resp¹ (₂∼₂ y≈y') (₂∼₂ x∼y) = ₂∼₂ (proj₁ resp₂ y≈y' x∼y)
    resp¹ (₂∼₂ y≈y') (₁∼₂ p)   = (₁∼₂ p)
    resp¹ (₁∼₂ ())   _

    resp² :  ∀ {y}
          → (flip (⊎ʳ P ∼₁ ∼₂) y) Respects (≈₁ ⊎-Rel ≈₂)
    resp² (₁∼₁ x≈x') (₁∼₁ x∼y) = ₁∼₁ (proj₂ resp₁ x≈x' x∼y)
    resp² (₂∼₂ x≈x') (₂∼₂ x∼y) = ₂∼₂ (proj₂ resp₂ x≈x' x∼y)
    resp² (₁∼₁ x≈x') (₁∼₂ p)   = (₁∼₂ p)
    resp² (₁∼₂ ())   _

  _⊎-substitutive_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                     Substitutive ∼₁ ℓ₃ → Substitutive ∼₂ ℓ₃ →
                     Substitutive (∼₁ ⊎-Rel ∼₂) ℓ₃
  subst₁ ⊎-substitutive subst₂ = subst
    where
    subst : Substitutive (_ ⊎-Rel _) _
    subst P (₁∼₁ x∼y) Px = subst₁ (λ z → P (inj₁ z)) x∼y Px
    subst P (₂∼₂ x∼y) Px = subst₂ (λ z → P (inj₂ z)) x∼y Px
    subst P (₁∼₂ ())  Px

  ⊎-decidable : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                Decidable ∼₁ → Decidable ∼₂ →
                ∀ {P} → (∀ {x y} → Dec (inj₁ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩ inj₂ y)) →
                Decidable (⊎ʳ P ∼₁ ∼₂)
  ⊎-decidable {∼₁ = ∼₁} {∼₂ = ∼₂} dec₁ dec₂ {P} dec₁₂ = dec
    where
    dec : Decidable (⊎ʳ P ∼₁ ∼₂)
    dec (inj₁ x) (inj₁ y) with dec₁ x y
    ...                   | yes x∼y = yes (₁∼₁ x∼y)
    ...                   | no  x≁y = no (x≁y ∘ drop-inj₁)
    dec (inj₂ x) (inj₂ y) with dec₂ x y
    ...                   | yes x∼y = yes (₂∼₂ x∼y)
    ...                   | no  x≁y = no (x≁y ∘ drop-inj₂)
    dec (inj₁ x) (inj₂ y) = dec₁₂
    dec (inj₂ x) (inj₁ y) = no (λ())

  _⊎-<-total_ : ∀ {ℓ₁ ℓ₂} {≤₁ : Rel A₁ ℓ₁} {≤₂ : Rel A₂ ℓ₂} →
                Total ≤₁ → Total ≤₂ → Total (≤₁ ⊎-< ≤₂)
  total₁ ⊎-<-total total₂ = total
    where
    total : Total (_ ⊎-< _)
    total (inj₁ x) (inj₁ y) = Sum.map ₁∼₁ ₁∼₁ $ total₁ x y
    total (inj₂ x) (inj₂ y) = Sum.map ₂∼₂ ₂∼₂ $ total₂ x y
    total (inj₁ x) (inj₂ y) = inj₁ (₁∼₂ _)
    total (inj₂ x) (inj₁ y) = inj₂ (₁∼₂ _)

  _⊎-<-trichotomous_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
                         {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
                       Trichotomous ≈₁ <₁ → Trichotomous ≈₂ <₂ →
                       Trichotomous (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
  _⊎-<-trichotomous_ {≈₁ = ≈₁} {<₁ = <₁} {≈₂ = ≈₂} {<₂ = <₂}
                     tri₁ tri₂ = tri
    where
    tri : Trichotomous (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
    tri (inj₁ x) (inj₂ y) = tri< (₁∼₂ _) ₁≁₂ (λ())
    tri (inj₂ x) (inj₁ y) = tri> (λ()) (λ()) (₁∼₂ _)
    tri (inj₁ x) (inj₁ y) with tri₁ x y
    ...                   | tri< x<y x≉y x≯y =
      tri< (₁∼₁ x<y)        (x≉y ∘ drop-inj₁) (x≯y ∘ drop-inj₁)
    ...                   | tri≈ x≮y x≈y x≯y =
      tri≈ (x≮y ∘ drop-inj₁) (₁∼₁ x≈y)    (x≯y ∘ drop-inj₁)
    ...                   | tri> x≮y x≉y x>y =
      tri> (x≮y ∘ drop-inj₁) (x≉y ∘ drop-inj₁) (₁∼₁ x>y)
    tri (inj₂ x) (inj₂ y) with tri₂ x y
    ...                   | tri< x<y x≉y x≯y =
      tri< (₂∼₂ x<y)        (x≉y ∘ drop-inj₂) (x≯y ∘ drop-inj₂)
    ...                   | tri≈ x≮y x≈y x≯y =
      tri≈ (x≮y ∘ drop-inj₂) (₂∼₂ x≈y)    (x≯y ∘ drop-inj₂)
    ...                   | tri> x≮y x≉y x>y =
      tri> (x≮y ∘ drop-inj₂) (x≉y ∘ drop-inj₂) (₂∼₂ x>y)

  ----------------------------------------------------------------------
  -- Some collections of properties which are preserved

  _⊎-isEquivalence_ : ∀ {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {≈₂ : Rel A₂ ℓ₂} →
                      IsEquivalence ≈₁ → IsEquivalence ≈₂ →
                      IsEquivalence (≈₁ ⊎-Rel ≈₂)
  eq₁ ⊎-isEquivalence eq₂ = record
    { refl  = refl  eq₁ ⊎-refl        refl  eq₂
    ; sym   = sym   eq₁ ⊎-symmetric   sym   eq₂
    ; trans = trans eq₁ ⊎-transitive  trans eq₂
    }
    where open IsEquivalence

  _⊎-isPreorder_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₁′}
                     {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {∼₂ : Rel A₂ ℓ₂′} →
                   IsPreorder ≈₁ ∼₁ → IsPreorder ≈₂ ∼₂ →
                   ∀ {P} → IsPreorder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ∼₁ ∼₂)
  pre₁ ⊎-isPreorder pre₂ = record
    { isEquivalence = isEquivalence pre₁ ⊎-isEquivalence
                      isEquivalence pre₂
    ; reflexive     = reflexive pre₁ ⊎-reflexive   reflexive pre₂
    ; trans         = trans     pre₁ ⊎-transitive  trans     pre₂
    }
    where open IsPreorder

  _⊎-isDecEquivalence_ : ∀ {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {≈₂ : Rel A₂ ℓ₂} →
                         IsDecEquivalence ≈₁ → IsDecEquivalence ≈₂ →
                         IsDecEquivalence (≈₁ ⊎-Rel ≈₂)
  eq₁ ⊎-isDecEquivalence eq₂ = record
    { isEquivalence = isEquivalence eq₁ ⊎-isEquivalence
                      isEquivalence eq₂
    ; _≟_           = ⊎-decidable (_≟_ eq₁) (_≟_ eq₂) (no ₁≁₂)
    }
    where open IsDecEquivalence

  _⊎-isPartialOrder_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
                         {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
                       IsPartialOrder ≈₁ ≤₁ → IsPartialOrder ≈₂ ≤₂ →
                       ∀ {P} → IsPartialOrder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ≤₁ ≤₂)
  po₁ ⊎-isPartialOrder po₂ = record
    { isPreorder = isPreorder po₁ ⊎-isPreorder    isPreorder po₂
    ; antisym    = antisym    po₁ ⊎-antisymmetric antisym    po₂
    }
    where open IsPartialOrder

  _⊎-isStrictPartialOrder_ :
    ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
    IsStrictPartialOrder ≈₁ <₁ → IsStrictPartialOrder ≈₂ <₂ →
    ∀ {P} → IsStrictPartialOrder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P <₁ <₂)
  spo₁ ⊎-isStrictPartialOrder spo₂ = record
    { isEquivalence = isEquivalence spo₁ ⊎-isEquivalence
                      isEquivalence spo₂
    ; irrefl        = irrefl   spo₁ ⊎-irreflexive irrefl   spo₂
    ; trans         = trans    spo₁ ⊎-transitive  trans    spo₂
    ; <-resp-≈      = <-resp-≈ spo₁ ⊎-≈-respects₂ <-resp-≈ spo₂
    }
    where open IsStrictPartialOrder

  _⊎-<-isTotalOrder_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
                         {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
                       IsTotalOrder ≈₁ ≤₁ → IsTotalOrder ≈₂ ≤₂ →
                       IsTotalOrder (≈₁ ⊎-Rel ≈₂) (≤₁ ⊎-< ≤₂)
  to₁ ⊎-<-isTotalOrder to₂ = record
    { isPartialOrder = isPartialOrder to₁ ⊎-isPartialOrder
                       isPartialOrder to₂
    ; total          = total to₁ ⊎-<-total total to₂
    }
    where open IsTotalOrder

  _⊎-<-isDecTotalOrder_ :
    ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
    IsDecTotalOrder ≈₁ ≤₁ → IsDecTotalOrder ≈₂ ≤₂ →
    IsDecTotalOrder (≈₁ ⊎-Rel ≈₂) (≤₁ ⊎-< ≤₂)
  to₁ ⊎-<-isDecTotalOrder to₂ = record
    { isTotalOrder = isTotalOrder to₁ ⊎-<-isTotalOrder isTotalOrder to₂
    ; _≟_          = ⊎-decidable (_≟_  to₁) (_≟_  to₂) (no ₁≁₂)
    ; _≤?_         = ⊎-decidable (_≤?_ to₁) (_≤?_ to₂) (yes (₁∼₂ _))
    }
    where open IsDecTotalOrder

  _⊎-<-isStrictTotalOrder_ :
    ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
    IsStrictTotalOrder ≈₁ <₁ → IsStrictTotalOrder ≈₂ <₂ →
    IsStrictTotalOrder (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
  sto₁ ⊎-<-isStrictTotalOrder sto₂ = record
    { isEquivalence = isEquivalence sto₁ ⊎-isEquivalence
                      isEquivalence sto₂
    ; trans         = trans    sto₁ ⊎-transitive     trans    sto₂
    ; compare       = compare  sto₁ ⊎-<-trichotomous compare  sto₂
    ; <-resp-≈      = <-resp-≈ sto₁ ⊎-≈-respects₂    <-resp-≈ sto₂
    }
    where open IsStrictTotalOrder

------------------------------------------------------------------------
-- The game can be taken even further...

_⊎-setoid_ : ∀ {s₁ s₂ s₃ s₄} →
             Setoid s₁ s₂ → Setoid s₃ s₄ → Setoid _ _
s₁ ⊎-setoid s₂ = record
  { isEquivalence = isEquivalence s₁ ⊎-isEquivalence isEquivalence s₂
  } where open Setoid

_⊎-preorder_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
               Preorder p₁ p₂ p₃ → Preorder p₄ p₅ p₆ → Preorder _ _ _
p₁ ⊎-preorder p₂ = record
  { _∼_          = _∼_        p₁ ⊎-Rel        _∼_        p₂
  ; isPreorder   = isPreorder p₁ ⊎-isPreorder isPreorder p₂
  } where open Preorder

_⊎-decSetoid_ : ∀ {s₁ s₂ s₃ s₄} →
                DecSetoid s₁ s₂ → DecSetoid s₃ s₄ → DecSetoid _ _
ds₁ ⊎-decSetoid ds₂ = record
  { isDecEquivalence = isDecEquivalence ds₁ ⊎-isDecEquivalence
                       isDecEquivalence ds₂
  } where open DecSetoid

_⊎-poset_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
            Poset p₁ p₂ p₃ → Poset p₄ p₅ p₆ → Poset _ _ _
po₁ ⊎-poset po₂ = record
  { _≤_            = _≤_ po₁ ⊎-Rel _≤_ po₂
  ; isPartialOrder = isPartialOrder po₁ ⊎-isPartialOrder
                     isPartialOrder po₂
  } where open Poset

_⊎-<-poset_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
              Poset p₁ p₂ p₃ → Poset p₄ p₅ p₆ → Poset _ _ _
po₁ ⊎-<-poset po₂ = record
  { _≤_            = _≤_ po₁ ⊎-< _≤_ po₂
  ; isPartialOrder = isPartialOrder po₁ ⊎-isPartialOrder
                     isPartialOrder po₂
  } where open Poset

_⊎-<-strictPartialOrder_ :
  ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
  StrictPartialOrder p₁ p₂ p₃ → StrictPartialOrder p₄ p₅ p₆ →
  StrictPartialOrder _ _ _
spo₁ ⊎-<-strictPartialOrder spo₂ = record
  { _<_                  = _<_ spo₁ ⊎-< _<_ spo₂
  ; isStrictPartialOrder = isStrictPartialOrder spo₁
                             ⊎-isStrictPartialOrder
                           isStrictPartialOrder spo₂
  } where open StrictPartialOrder

_⊎-<-totalOrder_ :
  ∀ {t₁ t₂ t₃ t₄ t₅ t₆} →
  TotalOrder t₁ t₂ t₃ → TotalOrder t₄ t₅ t₆ → TotalOrder _ _ _
to₁ ⊎-<-totalOrder to₂ = record
  { isTotalOrder = isTotalOrder to₁ ⊎-<-isTotalOrder isTotalOrder to₂
  } where open TotalOrder

_⊎-<-decTotalOrder_ :
  ∀ {t₁ t₂ t₃ t₄ t₅ t₆} →
  DecTotalOrder t₁ t₂ t₃ → DecTotalOrder t₄ t₅ t₆ → DecTotalOrder _ _ _
to₁ ⊎-<-decTotalOrder to₂ = record
  { isDecTotalOrder = isDecTotalOrder to₁ ⊎-<-isDecTotalOrder
                      isDecTotalOrder to₂
  } where open DecTotalOrder

_⊎-<-strictTotalOrder_ :
  ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
  StrictTotalOrder p₁ p₂ p₃ → StrictTotalOrder p₄ p₅ p₆ →
  StrictTotalOrder _ _ _
sto₁ ⊎-<-strictTotalOrder sto₂ = record
  { _<_                = _<_ sto₁ ⊎-< _<_ sto₂
  ; isStrictTotalOrder = isStrictTotalOrder sto₁
                           ⊎-<-isStrictTotalOrder
                         isStrictTotalOrder sto₂
  } where open StrictTotalOrder

------------------------------------------------------------------------
-- Some properties related to "relatedness"

private

  to-cong : ∀ {a b} {A : Set a} {B : Set b} →
            (_≡_ ⊎-Rel _≡_) ⇒ _≡_ {A = A ⊎ B}
  to-cong (₁∼₂ ())
  to-cong (₁∼₁ P.refl) = P.refl
  to-cong (₂∼₂ P.refl) = P.refl

  from-cong : ∀ {a b} {A : Set a} {B : Set b} →
              _≡_ {A = A ⊎ B} ⇒ (_≡_ ⊎-Rel _≡_)
  from-cong P.refl = P.refl ⊎-refl P.refl

⊎-Rel↔≡ : ∀ {a b} (A : Set a) (B : Set b) →
          Inverse (P.setoid A ⊎-setoid P.setoid B) (P.setoid (A ⊎ B))
⊎-Rel↔≡ _ _ = record
  { to         = record { _⟨$⟩_ = id; cong = to-cong   }
  ; from       = record { _⟨$⟩_ = id; cong = from-cong }
  ; inverse-of = record
    { left-inverse-of  = λ _ → P.refl ⊎-refl P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

_⊎-≟_ : ∀ {a b} {A : Set a} {B : Set b} →
        Decidable {A = A} _≡_ → Decidable {A = B} _≡_ →
        Decidable {A = A ⊎ B} _≡_
(dec₁ ⊎-≟ dec₂) s₁ s₂ = Dec.map′ to-cong from-cong (s₁ ≟ s₂)
  where
  open DecSetoid (P.decSetoid dec₁ ⊎-decSetoid P.decSetoid dec₂)

_⊎-⟶_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  A ⟶ B → C ⟶ D → (A ⊎-setoid C) ⟶ (B ⊎-setoid D)
_⊎-⟶_ {A = A} {B} {C} {D} f g = record
  { _⟨$⟩_ = fg
  ; cong  = fg-cong
  }
  where
  open Setoid (A ⊎-setoid C) using () renaming (_≈_ to _≈AC_)
  open Setoid (B ⊎-setoid D) using () renaming (_≈_ to _≈BD_)

  fg = Sum.map (_⟨$⟩_ f) (_⟨$⟩_ g)

  fg-cong : _≈AC_ =[ fg ]⇒ _≈BD_
  fg-cong (₁∼₂ ())
  fg-cong (₁∼₁ x∼₁y) = ₁∼₁ $ F.cong f x∼₁y
  fg-cong (₂∼₂ x∼₂y) = ₂∼₂ $ F.cong g x∼₂y

_⊎-equivalence_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Equivalence A B → Equivalence C D →
  Equivalence (A ⊎-setoid C) (B ⊎-setoid D)
A⇔B ⊎-equivalence C⇔D = record
  { to   = to   A⇔B ⊎-⟶ to   C⇔D
  ; from = from A⇔B ⊎-⟶ from C⇔D
  } where open Equivalence

_⊎-⇔_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ⇔ B → C ⇔ D → (A ⊎ C) ⇔ (B ⊎ D)
_⊎-⇔_ {A = A} {B} {C} {D} A⇔B C⇔D =
  Inverse.equivalence (⊎-Rel↔≡ B D) ⟨∘⟩
  A⇔B ⊎-equivalence C⇔D ⟨∘⟩
  Eq.sym (Inverse.equivalence (⊎-Rel↔≡ A C))
  where open Eq using () renaming (_∘_ to _⟨∘⟩_)

_⊎-injection_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Injection A B → Injection C D →
  Injection (A ⊎-setoid C) (B ⊎-setoid D)
_⊎-injection_ {A = A} {B} {C} {D} A↣B C↣D = record
  { to        = to A↣B ⊎-⟶ to C↣D
  ; injective = inj _ _
  }
  where
  open Injection
  open Setoid (A ⊎-setoid C) using () renaming (_≈_ to _≈AC_)
  open Setoid (B ⊎-setoid D) using () renaming (_≈_ to _≈BD_)

  inj : ∀ x y →
        (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ x ≈BD (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ y →
        x ≈AC y
  inj (inj₁ x) (inj₁ y) (₁∼₁ x∼₁y) = ₁∼₁ (injective A↣B x∼₁y)
  inj (inj₂ x) (inj₂ y) (₂∼₂ x∼₂y) = ₂∼₂ (injective C↣D x∼₂y)
  inj (inj₁ x) (inj₂ y) (₁∼₂ ())
  inj (inj₂ x) (inj₁ y) ()

_⊎-↣_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↣ B → C ↣ D → (A ⊎ C) ↣ (B ⊎ D)
_⊎-↣_ {A = A} {B} {C} {D} A↣B C↣D =
  Inverse.injection (⊎-Rel↔≡ B D) ⟨∘⟩
  A↣B ⊎-injection C↣D ⟨∘⟩
  Inverse.injection (Inv.sym (⊎-Rel↔≡ A C))
  where open Inj using () renaming (_∘_ to _⟨∘⟩_)

_⊎-left-inverse_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  LeftInverse A B → LeftInverse C D →
  LeftInverse (A ⊎-setoid C) (B ⊎-setoid D)
A↞B ⊎-left-inverse C↞D = record
  { to              = Equivalence.to eq
  ; from            = Equivalence.from eq
  ; left-inverse-of = [ ₁∼₁ ∘ left-inverse-of A↞B
                      , ₂∼₂ ∘ left-inverse-of C↞D
                      ]
  }
  where
  open LeftInverse
  eq = LeftInverse.equivalence A↞B ⊎-equivalence
       LeftInverse.equivalence C↞D

_⊎-↞_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↞ B → C ↞ D → (A ⊎ C) ↞ (B ⊎ D)
_⊎-↞_ {A = A} {B} {C} {D} A↞B C↞D =
  Inverse.left-inverse (⊎-Rel↔≡ B D) ⟨∘⟩
  A↞B ⊎-left-inverse C↞D ⟨∘⟩
  Inverse.left-inverse (Inv.sym (⊎-Rel↔≡ A C))
  where open LeftInv using () renaming (_∘_ to _⟨∘⟩_)

_⊎-surjection_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Surjection A B → Surjection C D →
  Surjection (A ⊎-setoid C) (B ⊎-setoid D)
A↠B ⊎-surjection C↠D = record
  { to         = LeftInverse.from inv
  ; surjective = record
    { from             = LeftInverse.to inv
    ; right-inverse-of = LeftInverse.left-inverse-of inv
    }
  }
  where
  open Surjection
  inv = right-inverse A↠B ⊎-left-inverse right-inverse C↠D

_⊎-↠_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↠ B → C ↠ D → (A ⊎ C) ↠ (B ⊎ D)
_⊎-↠_ {A = A} {B} {C} {D} A↠B C↠D =
  Inverse.surjection (⊎-Rel↔≡ B D) ⟨∘⟩
  A↠B ⊎-surjection C↠D ⟨∘⟩
  Inverse.surjection (Inv.sym (⊎-Rel↔≡ A C))
  where open Surj using () renaming (_∘_ to _⟨∘⟩_)

_⊎-inverse_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Inverse A B → Inverse C D → Inverse (A ⊎-setoid C) (B ⊎-setoid D)
A↔B ⊎-inverse C↔D = record
  { to         = Surjection.to   surj
  ; from       = Surjection.from surj
  ; inverse-of = record
    { left-inverse-of  = LeftInverse.left-inverse-of inv
    ; right-inverse-of = Surjection.right-inverse-of surj
    }
  }
  where
  open Inverse
  surj = Inverse.surjection   A↔B ⊎-surjection
         Inverse.surjection   C↔D
  inv  = Inverse.left-inverse A↔B ⊎-left-inverse
         Inverse.left-inverse C↔D

_⊎-↔_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
_⊎-↔_ {A = A} {B} {C} {D} A↔B C↔D =
  ⊎-Rel↔≡ B D ⟨∘⟩ A↔B ⊎-inverse C↔D ⟨∘⟩ Inv.sym (⊎-Rel↔≡ A C)
  where open Inv using () renaming (_∘_ to _⟨∘⟩_)

_⊎-cong_ : ∀ {k a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
           A ∼[ k ] B → C ∼[ k ] D → (A ⊎ C) ∼[ k ] (B ⊎ D)
_⊎-cong_ {implication}         = Sum.map
_⊎-cong_ {reverse-implication} = λ f g → lam (Sum.map (app-← f) (app-← g))
_⊎-cong_ {equivalence}         = _⊎-⇔_
_⊎-cong_ {injection}           = _⊎-↣_
_⊎-cong_ {reverse-injection}   = λ f g → lam (app-↢ f ⊎-↣ app-↢ g)
_⊎-cong_ {left-inverse}        = _⊎-↞_
_⊎-cong_ {surjection}          = _⊎-↠_
_⊎-cong_ {bijection}           = _⊎-↔_