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

{-# OPTIONS --without-K --safe #-}

module Data.Sum.Relation.Binary.Pointwise where

open import Data.Product using (_,_)
open import Data.Sum.Base as Sum
open import Data.Sum.Properties
open import Level using (_⊔_)
open import Function.Base using (_∘_; id)
open import Function.Inverse using (Inverse)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

data Pointwise {a b c d r s}
               {A : Set a} {B : Set b} {C : Set c} {D : Set d}
               (R : REL A C r) (S : REL B D s)
               : REL (A  B) (C  D) (a  b  c  d  r  s) 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)

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

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂}
         where

  drop-inj₁ :  {x y}  Pointwise ∼₁ ∼₂ (inj₁ x) (inj₁ y)  ∼₁ x y
  drop-inj₁ (inj₁ x) = x

  drop-inj₂ :  {x y}  Pointwise ∼₁ ∼₂ (inj₂ x) (inj₂ y)  ∼₂ x y
  drop-inj₂ (inj₂ x) = x

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

  ⊎-symmetric : Symmetric ∼₁  Symmetric ∼₂ 
                Symmetric (Pointwise ∼₁ ∼₂)
  ⊎-symmetric sym₁ sym₂ (inj₁ x) = inj₁ (sym₁ x)
  ⊎-symmetric sym₁ sym₂ (inj₂ x) = inj₂ (sym₂ x)

  ⊎-transitive : Transitive ∼₁  Transitive ∼₂ 
                 Transitive (Pointwise ∼₁ ∼₂)
  ⊎-transitive trans₁ trans₂ (inj₁ x) (inj₁ y) = inj₁ (trans₁ x y)
  ⊎-transitive trans₁ trans₂ (inj₂ x) (inj₂ y) = inj₂ (trans₂ x y)

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

  ⊎-substitutive :  {ℓ₃}  Substitutive ∼₁ ℓ₃  Substitutive ∼₂ ℓ₃ 
                   Substitutive (Pointwise ∼₁ ∼₂) ℓ₃
  ⊎-substitutive subst₁ subst₂ P (inj₁ x) = subst₁ (P  inj₁) x
  ⊎-substitutive subst₁ subst₂ P (inj₂ x) = subst₂ (P  inj₂) x

  ⊎-decidable : Decidable ∼₁  Decidable ∼₂ 
                Decidable (Pointwise ∼₁ ∼₂)
  ⊎-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)

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂}
         {ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄} where

  ⊎-reflexive : ≈₁  ∼₁  ≈₂  ∼₂ 
                (Pointwise ≈₁ ≈₂)  (Pointwise ∼₁ ∼₂)
  ⊎-reflexive refl₁ refl₂ (inj₁ x) = inj₁ (refl₁ x)
  ⊎-reflexive refl₁ refl₂ (inj₂ x) = inj₂ (refl₂ x)

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

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

  ⊎-respectsˡ : ∼₁ Respectsˡ ≈₁  ∼₂ Respectsˡ ≈₂ 
                (Pointwise ∼₁ ∼₂) 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ʳ : ∼₁ Respectsʳ ≈₁  ∼₂ Respectsʳ ≈₂ 
                (Pointwise ∼₁ ∼₂) 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₂ : ∼₁ Respects₂ ≈₁  ∼₂ Respects₂ ≈₂ 
                (Pointwise ∼₁ ∼₂) Respects₂ (Pointwise ≈₁ ≈₂)
  ⊎-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-respectsʳ r₁ r₂ , ⊎-respectsˡ l₁ l₂

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

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {≈₂ : Rel A₂ ℓ₂}
         where

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

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₂}
         {ℓ₃ ℓ₄} {≈₂ : Rel A₂ ℓ₃} {∼₂ : Rel A₂ ℓ₄} where

  ⊎-isPreorder : IsPreorder ≈₁ ∼₁  IsPreorder ≈₂ ∼₂ 
                 IsPreorder (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-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 ≈₁ ∼₁ 
                     IsPartialOrder ≈₂ ∼₂ 
                     IsPartialOrder
                       (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-isPartialOrder po₁ po₂ = record
    { isPreorder = ⊎-isPreorder (isPreorder po₁) (isPreorder po₂)
    ; antisym    = ⊎-antisymmetric (antisym po₁) (antisym    po₂)
    }
    where open IsPartialOrder

  ⊎-isStrictPartialOrder : IsStrictPartialOrder ≈₁ ∼₁ 
                           IsStrictPartialOrder ≈₂ ∼₂ 
                           IsStrictPartialOrder
                             (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-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

module _ {a b c d} where

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

  -- Some additional notation for combining setoids
  infix 4 _⊎ₛ_
  _⊎ₛ_ : Setoid a b  Setoid c d  Setoid _ _
  _⊎ₛ_ = ⊎-setoid

module _ {a b c d e f} where

  ⊎-preorder : Preorder a b c  Preorder d e f  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

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

module _ {a b} {A : Set a} {B : Set b} where

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

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

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