{-# 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 Data.Sum.Properties
open import Level using (Level; _⊔_)
open import Function.Base using (const; _∘_; id)
open import Function.Bundles using (Inverse; mk↔)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as P
private
variable
a b c d ℓ₁ ℓ₂ ℓ₃ ℓ : Level
A B C D : Set ℓ
R S T U : REL A B ℓ
≈₁ ≈₂ : Rel A ℓ
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)
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)
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
⊎-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₂
⊎-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
⊎-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
infix 4 _⊎ₛ_
_⊎ₛ_ : Setoid a b → Setoid c d → Setoid _ _
_⊎ₛ_ = ⊎-setoid
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 : Set a) (B : Set b) →
Inverse (P.setoid A ⊎ₛ P.setoid B) (P.setoid (A ⊎ B))
Pointwise-≡↔≡ _ _ = record
{ to = id
; from = id
; to-cong = Pointwise-≡⇒≡
; from-cong = ≡⇒Pointwise-≡
; inverse = Pointwise-≡⇒≡ , ≡⇒Pointwise-≡
}