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

module Data.Sum.Relation.General where

open import Data.Sum as Sum
open import Data.Product
open import Data.Unit.Base 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₂
    }
    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}           = _⊎-↔_