    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Pointwise sum
    ------------------------------------------------------------------------

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

    module Data.Sum.Relation.Binary.Pointwise where

    open import Data.Product.Base using (_,_)
    open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
    open import Induction.WellFounded
    open import Level using (Level; _⊔_)
    open import Function.Base using (const; _∘_; id)
    open import Function.Bundles using (Inverse; mk↔)
    open import Relation.Nullary.Decidable.Core as Dec using (yes; no; map′)
    open import Relation.Nullary.Negation.Core using (¬_)
    open import Relation.Binary
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
    import Relation.Binary.PropositionalEquality.Properties as ≡

    private
      variable
        a b c d ℓ₁ ℓ₂ ℓ₃ ℓ : Level
        A B C D : Set ℓ
        R S T U : REL A B ℓ
        ≈₁ ≈₂ : Rel A ℓ

    ------------------------------------------------------------------------
    -- Definition

    data Pointwise {A : Set a} {B : Set b} {C : Set c} {D : Set d}
                   (R : REL A C ℓ₁) (S : REL B D ℓ₂)
                   : REL (A ⊎ B) (C ⊎ D) (a ⊔ b ⊔ c ⊔ d ⊔ ℓ₁ ⊔ ℓ₂) where
      inj₁ : ∀ {a c} → R a c → Pointwise R S (inj₁ a) (inj₁ c)
      inj₂ : ∀ {b d} → S b d → Pointwise R S (inj₂ b) (inj₂ d)

    ----------------------------------------------------------------------
    -- Functions

    map : ∀ {f : A → C} {g : B → D} →
          R =[ f ]⇒ T → S =[ g ]⇒ U →
          Pointwise R S =[ Sum.map f g ]⇒ Pointwise T U
    map R⇒T _ (inj₁ x) = inj₁ (R⇒T x)
    map _ S⇒U (inj₂ x) = inj₂ (S⇒U x)

    ------------------------------------------------------------------------
    -- Relational properties

    drop-inj₁ : ∀ {x y} → Pointwise R S (inj₁ x) (inj₁ y) → R x y
    drop-inj₁ (inj₁ x) = x

    drop-inj₂ : ∀ {x y} → Pointwise R S (inj₂ x) (inj₂ y) → S x y
    drop-inj₂ (inj₂ x) = x

    ⊎-refl : Reflexive R → Reflexive S → Reflexive (Pointwise R S)
    ⊎-refl refl₁ refl₂ {inj₁ x} = inj₁ refl₁
    ⊎-refl refl₁ refl₂ {inj₂ y} = inj₂ refl₂

    ⊎-symmetric : Symmetric R → Symmetric S →
                  Symmetric (Pointwise R S)
    ⊎-symmetric sym₁ sym₂ (inj₁ x) = inj₁ (sym₁ x)
    ⊎-symmetric sym₁ sym₂ (inj₂ x) = inj₂ (sym₂ x)

    ⊎-transitive : Transitive R → Transitive S →
                   Transitive (Pointwise R S)
    ⊎-transitive trans₁ trans₂ (inj₁ x) (inj₁ y) = inj₁ (trans₁ x y)
    ⊎-transitive trans₁ trans₂ (inj₂ x) (inj₂ y) = inj₂ (trans₂ x y)

    ⊎-asymmetric : Asymmetric R → Asymmetric S →
                   Asymmetric (Pointwise R S)
    ⊎-asymmetric asym₁ asym₂ (inj₁ x) = λ { (inj₁ y) → asym₁ x y }
    ⊎-asymmetric asym₁ asym₂ (inj₂ x) = λ { (inj₂ y) → asym₂ x y }

    ⊎-substitutive : Substitutive R ℓ₃ → Substitutive S ℓ₃ →
                     Substitutive (Pointwise R S) ℓ₃
    ⊎-substitutive subst₁ subst₂ P (inj₁ x) = subst₁ (P ∘ inj₁) x
    ⊎-substitutive subst₁ subst₂ P (inj₂ x) = subst₂ (P ∘ inj₂) x

    ⊎-decidable : Decidable R → Decidable S → Decidable (Pointwise R S)
    ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₁ y) = Dec.map′ inj₁ drop-inj₁ (x ≟₁ y)
    ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₂ y) = no λ()
    ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₁ y) = no λ()
    ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₂ y) = Dec.map′ inj₂ drop-inj₂ (x ≟₂ y)

    ⊎-reflexive : ≈₁ ⇒ R → ≈₂ ⇒ S →
                  (Pointwise ≈₁ ≈₂) ⇒ (Pointwise R S)
    ⊎-reflexive refl₁ refl₂ (inj₁ x) = inj₁ (refl₁ x)
    ⊎-reflexive refl₁ refl₂ (inj₂ x) = inj₂ (refl₂ x)

    ⊎-irreflexive : Irreflexive ≈₁ R → Irreflexive ≈₂ S →
                    Irreflexive (Pointwise ≈₁ ≈₂) (Pointwise R S)
    ⊎-irreflexive irrefl₁ irrefl₂ (inj₁ x) (inj₁ y) = irrefl₁ x y
    ⊎-irreflexive irrefl₁ irrefl₂ (inj₂ x) (inj₂ y) = irrefl₂ x y

    ⊎-wellFounded : WellFounded ≈₁ → WellFounded ≈₂ → WellFounded (Pointwise ≈₁ ≈₂)
    ⊎-wellFounded {≈₁ = ≈₁} {≈₂ = ≈₂} wf₁ wf₂ x = acc (⊎-acc x)
      where
      ⊎-acc₁ : ∀ {x} → Acc ≈₁ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) (inj₁ x)
      ⊎-acc₁ (acc rec) (inj₁ x≈₁y) = acc (⊎-acc₁ (rec x≈₁y))

      ⊎-acc₂ : ∀ {x} → Acc ≈₂ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) (inj₂ x)
      ⊎-acc₂ (acc rec) (inj₂ x≈₂y) = acc (⊎-acc₂ (rec x≈₂y))

      ⊎-acc  : ∀ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) x
      ⊎-acc (inj₁ x) = ⊎-acc₁ (wf₁ x)
      ⊎-acc (inj₂ x) = ⊎-acc₂ (wf₂ x)

    ⊎-antisymmetric : Antisymmetric ≈₁ R → Antisymmetric ≈₂ S →
                      Antisymmetric (Pointwise ≈₁ ≈₂) (Pointwise R S)
    ⊎-antisymmetric antisym₁ antisym₂ (inj₁ x) (inj₁ y) = inj₁ (antisym₁ x y)
    ⊎-antisymmetric antisym₁ antisym₂ (inj₂ x) (inj₂ y) = inj₂ (antisym₂ x y)

    ⊎-respectsˡ : R Respectsˡ ≈₁ → S Respectsˡ ≈₂ →
                  (Pointwise R S) Respectsˡ (Pointwise ≈₁ ≈₂)
    ⊎-respectsˡ resp₁ resp₂ (inj₁ x) (inj₁ y) = inj₁ (resp₁ x y)
    ⊎-respectsˡ resp₁ resp₂ (inj₂ x) (inj₂ y) = inj₂ (resp₂ x y)

    ⊎-respectsʳ : R Respectsʳ ≈₁ → S Respectsʳ ≈₂ →
                  (Pointwise R S) Respectsʳ (Pointwise ≈₁ ≈₂)
    ⊎-respectsʳ resp₁ resp₂ (inj₁ x) (inj₁ y) = inj₁ (resp₁ x y)
    ⊎-respectsʳ resp₁ resp₂ (inj₂ x) (inj₂ y) = inj₂ (resp₂ x y)

    ⊎-respects₂ : R Respects₂ ≈₁ → S Respects₂ ≈₂ →
                  (Pointwise R S) Respects₂ (Pointwise ≈₁ ≈₂)
    ⊎-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-respectsʳ r₁ r₂ , ⊎-respectsˡ l₁ l₂

    ------------------------------------------------------------------------
    -- Structures

    ⊎-isEquivalence : IsEquivalence ≈₁ → IsEquivalence ≈₂ →
                      IsEquivalence (Pointwise ≈₁ ≈₂)
    ⊎-isEquivalence eq₁ eq₂ = record
      { refl  = ⊎-refl       (refl  eq₁) (refl  eq₂)
      ; sym   = ⊎-symmetric  (sym   eq₁) (sym   eq₂)
      ; trans = ⊎-transitive (trans eq₁) (trans eq₂)
      } where open IsEquivalence

    ⊎-isDecEquivalence : IsDecEquivalence ≈₁ → IsDecEquivalence ≈₂ →
                         IsDecEquivalence (Pointwise ≈₁ ≈₂)
    ⊎-isDecEquivalence eq₁ eq₂ = record
      { isEquivalence =
          ⊎-isEquivalence (isEquivalence eq₁) (isEquivalence eq₂)
      ; _≟_           = ⊎-decidable (_≟_ eq₁) (_≟_ eq₂)
      } where open IsDecEquivalence

    ⊎-isPreorder : IsPreorder ≈₁ R → IsPreorder ≈₂ S →
                   IsPreorder (Pointwise ≈₁ ≈₂) (Pointwise R S)
    ⊎-isPreorder pre₁ pre₂ = record
      { isEquivalence =
          ⊎-isEquivalence (isEquivalence pre₁) (isEquivalence pre₂)
      ; reflexive     = ⊎-reflexive (reflexive pre₁) (reflexive pre₂)
      ; trans         = ⊎-transitive (trans pre₁) (trans pre₂)
      } where open IsPreorder

    ⊎-isPartialOrder : IsPartialOrder ≈₁ R → IsPartialOrder ≈₂ S →
                       IsPartialOrder
                         (Pointwise ≈₁ ≈₂) (Pointwise R S)
    ⊎-isPartialOrder po₁ po₂ = record
      { isPreorder = ⊎-isPreorder (isPreorder po₁) (isPreorder po₂)
      ; antisym    = ⊎-antisymmetric (antisym po₁) (antisym    po₂)
      } where open IsPartialOrder

    ⊎-isStrictPartialOrder : IsStrictPartialOrder ≈₁ R →
                             IsStrictPartialOrder ≈₂ S →
                             IsStrictPartialOrder
                               (Pointwise ≈₁ ≈₂) (Pointwise R S)
    ⊎-isStrictPartialOrder spo₁ spo₂ = record
      { isEquivalence =
          ⊎-isEquivalence (isEquivalence spo₁) (isEquivalence spo₂)
      ; irrefl        = ⊎-irreflexive (irrefl   spo₁) (irrefl   spo₂)
      ; trans         = ⊎-transitive  (trans    spo₁) (trans    spo₂)
      ; <-resp-≈      = ⊎-respects₂   (<-resp-≈ spo₁) (<-resp-≈ spo₂)
      } where open IsStrictPartialOrder

    ------------------------------------------------------------------------
    -- Bundles

    ⊎-setoid : Setoid a b → Setoid c d → Setoid _ _
    ⊎-setoid s₁ s₂ = record
      { isEquivalence =
          ⊎-isEquivalence (isEquivalence s₁) (isEquivalence s₂)
      } where open Setoid

    ⊎-decSetoid : DecSetoid a b → DecSetoid c d → DecSetoid _ _
    ⊎-decSetoid ds₁ ds₂ = record
      { isDecEquivalence =
          ⊎-isDecEquivalence (isDecEquivalence ds₁) (isDecEquivalence ds₂)
      } where open DecSetoid

    ⊎-preorder : Preorder a b ℓ₁ → Preorder c d ℓ₂ → Preorder _ _ _
    ⊎-preorder p₁ p₂ = record
      { isPreorder   =
          ⊎-isPreorder (isPreorder p₁) (isPreorder p₂)
      } where open Preorder

    ⊎-poset : Poset a b c → Poset a b c → Poset _ _ _
    ⊎-poset po₁ po₂ = record
      { isPartialOrder =
          ⊎-isPartialOrder (isPartialOrder po₁) (isPartialOrder po₂)
      } where open Poset

    ------------------------------------------------------------------------
    -- Additional notation

    -- Infix combining setoids
    infix 4 _⊎ₛ_
    _⊎ₛ_ : Setoid a b → Setoid c d → Setoid _ _
    _⊎ₛ_ = ⊎-setoid

    ------------------------------------------------------------------------
    -- The propositional equality setoid over products can be
    -- decomposed using Pointwise

    Pointwise-≡⇒≡ : (Pointwise _≡_ _≡_) ⇒ _≡_ {A = A ⊎ B}
    Pointwise-≡⇒≡ (inj₁ x) = ≡.cong inj₁ x
    Pointwise-≡⇒≡ (inj₂ x) = ≡.cong inj₂ x

    ≡⇒Pointwise-≡ : _≡_ {A = A ⊎ B} ⇒ (Pointwise _≡_ _≡_)
    ≡⇒Pointwise-≡ ≡.refl = ⊎-refl ≡.refl ≡.refl

    Pointwise-≡↔≡ : (A : Set a) (B : Set b) →
                     Inverse (≡.setoid A ⊎ₛ ≡.setoid B) (≡.setoid (A ⊎ B))
    Pointwise-≡↔≡ _ _ = record
      { to        = id
      ; from      = id
      ; to-cong   = Pointwise-≡⇒≡
      ; from-cong = ≡⇒Pointwise-≡
      ; inverse   = Pointwise-≡⇒≡ , ≡⇒Pointwise-≡
      }