------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise products of binary relations
------------------------------------------------------------------------

module Relation.Binary.Product.Pointwise where

open import Data.Product as Prod
open import Data.Sum
open import Data.Unit.Base using ()
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; _↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)
open import Level
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

  infixr 2 _×-Rel_

  _×-Rel_ : Rel A₁ ℓ₁  Rel A₂ ℓ₂  Rel (A₁ × A₂) _
  _∼₁_ ×-Rel _∼₂_ = (_∼₁_ on proj₁) -×- (_∼₂_ on proj₂)

  -- Some properties which are preserved by ×-Rel (under certain
  -- assumptions).

  _×-reflexive_ :
     {_≈₁_ _∼₁_ _≈₂_ _∼₂_} 
    _≈₁_  _∼₁_  _≈₂_  _∼₂_  (_≈₁_ ×-Rel _≈₂_)  (_∼₁_ ×-Rel _∼₂_)
  refl₁ ×-reflexive refl₂ = λ x≈y 
    (refl₁ (proj₁ x≈y) , refl₂ (proj₂ x≈y))

  _×-refl_ :
     {_∼₁_ _∼₂_} 
    Reflexive _∼₁_  Reflexive _∼₂_  Reflexive (_∼₁_ ×-Rel _∼₂_)
  refl₁ ×-refl refl₂ = (refl₁ , refl₂)

  ×-irreflexive₁ :
     {_≈₁_ _<₁_ _≈₂_ _<₂_} 
    Irreflexive _≈₁_ _<₁_ 
    Irreflexive (_≈₁_ ×-Rel _≈₂_) (_<₁_ ×-Rel _<₂_)
  ×-irreflexive₁ ir = λ x≈y x<y  ir (proj₁ x≈y) (proj₁ x<y)

  ×-irreflexive₂ :
     {_≈₁_ _<₁_ _≈₂_ _<₂_} 
    Irreflexive _≈₂_ _<₂_ 
    Irreflexive (_≈₁_ ×-Rel _≈₂_) (_<₁_ ×-Rel _<₂_)
  ×-irreflexive₂ ir = λ x≈y x<y  ir (proj₂ x≈y) (proj₂ x<y)

  _×-symmetric_ :
     {_∼₁_ _∼₂_} 
    Symmetric _∼₁_  Symmetric _∼₂_  Symmetric (_∼₁_ ×-Rel _∼₂_)
  sym₁ ×-symmetric sym₂ = λ x∼y  sym₁ (proj₁ x∼y) , sym₂ (proj₂ x∼y)

  _×-transitive_ :  {_∼₁_ _∼₂_} 
                   Transitive _∼₁_  Transitive _∼₂_ 
                   Transitive (_∼₁_ ×-Rel _∼₂_)
  trans₁ ×-transitive trans₂ = λ x∼y y∼z 
    trans₁ (proj₁ x∼y) (proj₁ y∼z) ,
    trans₂ (proj₂ x∼y) (proj₂ y∼z)

  _×-antisymmetric_ :
     {_≈₁_ _≤₁_ _≈₂_ _≤₂_} 
    Antisymmetric _≈₁_ _≤₁_  Antisymmetric _≈₂_ _≤₂_ 
    Antisymmetric (_≈₁_ ×-Rel _≈₂_) (_≤₁_ ×-Rel _≤₂_)
  antisym₁ ×-antisymmetric antisym₂ = λ x≤y y≤x 
    ( antisym₁ (proj₁ x≤y) (proj₁ y≤x)
    , antisym₂ (proj₂ x≤y) (proj₂ y≤x) )

  ×-asymmetric₁ :
     {_<₁_ _∼₂_}  Asymmetric _<₁_  Asymmetric (_<₁_ ×-Rel _∼₂_)
  ×-asymmetric₁ asym₁ = λ x<y y<x  asym₁ (proj₁ x<y) (proj₁ y<x)

  ×-asymmetric₂ :
     {_∼₁_ _<₂_}  Asymmetric _<₂_  Asymmetric (_∼₁_ ×-Rel _<₂_)
  ×-asymmetric₂ asym₂ = λ x<y y<x  asym₂ (proj₂ x<y) (proj₂ y<x)

  _×-≈-respects₂_ :  {_≈₁_ _∼₁_ _≈₂_ _∼₂_} 
                    _∼₁_ Respects₂ _≈₁_  _∼₂_ Respects₂ _≈₂_ 
                    (_∼₁_ ×-Rel _∼₂_) Respects₂ (_≈₁_ ×-Rel _≈₂_)
  _×-≈-respects₂_
    {_≈₁_ = _≈₁_} {_∼₁_ = _∼₁_} {_≈₂_ = _≈₂_} {_∼₂_ = _∼₂_}
    resp₁ resp₂ =
     {x y z}  resp¹ {x} {y} {z}) ,
     {x y z}  resp² {x} {y} {z})
    where
    _∼_ = _∼₁_ ×-Rel _∼₂_

    resp¹ :  {x}  (_∼_ x) Respects (_≈₁_ ×-Rel _≈₂_)
    resp¹ y≈y' x∼y = proj₁ resp₁ (proj₁ y≈y') (proj₁ x∼y) ,
                     proj₁ resp₂ (proj₂ y≈y') (proj₂ x∼y)

    resp² :  {y}  (flip _∼_ y) Respects (_≈₁_ ×-Rel _≈₂_)
    resp² x≈x' x∼y = proj₂ resp₁ (proj₁ x≈x') (proj₁ x∼y) ,
                     proj₂ resp₂ (proj₂ x≈x') (proj₂ x∼y)

  ×-total :
     {_∼₁_ _∼₂_} 
    Symmetric _∼₁_  Total _∼₁_  Total _∼₂_  Total (_∼₁_ ×-Rel _∼₂_)
  ×-total {_∼₁_ = _∼₁_} {_∼₂_ = _∼₂_} sym₁ total₁ total₂ = total
    where
    total : Total (_∼₁_ ×-Rel _∼₂_)
    total x y with total₁ (proj₁ x) (proj₁ y)
                 | total₂ (proj₂ x) (proj₂ y)
    ... | inj₁ x₁∼y₁ | inj₁ x₂∼y₂ = inj₁ (     x₁∼y₁ , x₂∼y₂)
    ... | inj₁ x₁∼y₁ | inj₂ y₂∼x₂ = inj₂ (sym₁ x₁∼y₁ , y₂∼x₂)
    ... | inj₂ y₁∼x₁ | inj₂ y₂∼x₂ = inj₂ (     y₁∼x₁ , y₂∼x₂)
    ... | inj₂ y₁∼x₁ | inj₁ x₂∼y₂ = inj₁ (sym₁ y₁∼x₁ , x₂∼y₂)

  _×-decidable_ :
     {_∼₁_ _∼₂_} 
    Decidable _∼₁_  Decidable _∼₂_  Decidable (_∼₁_ ×-Rel _∼₂_)
  dec₁ ×-decidable dec₂ = λ x y 
    dec₁ (proj₁ x) (proj₁ y)
      ×-dec
    dec₂ (proj₂ x) (proj₂ y)

  -- Some collections of properties which are preserved by ×-Rel.

  _×-isEquivalence_ :  {_≈₁_ _≈₂_} 
                      IsEquivalence _≈₁_  IsEquivalence _≈₂_ 
                      IsEquivalence (_≈₁_ ×-Rel _≈₂_)
  _×-isEquivalence_ {_≈₁_ = _≈₁_} {_≈₂_ = _≈₂_} eq₁ eq₂ = record
    { refl  = λ {x} 
              _×-refl_        {_∼₁_ = _≈₁_} {_∼₂_ = _≈₂_}
                              (refl  eq₁) (refl  eq₂) {x}
    ; sym   = λ {x y} 
              _×-symmetric_   {_∼₁_ = _≈₁_} {_∼₂_ = _≈₂_}
                              (sym   eq₁) (sym   eq₂) {x} {y}
    ; trans = λ {x y z} 
              _×-transitive_  {_∼₁_ = _≈₁_} {_∼₂_ = _≈₂_}
                              (trans eq₁) (trans eq₂) {x} {y} {z}
    }
    where open IsEquivalence

  _×-isPreorder_ :  {_≈₁_ _∼₁_ _≈₂_ _∼₂_} 
                   IsPreorder _≈₁_ _∼₁_  IsPreorder _≈₂_ _∼₂_ 
                   IsPreorder (_≈₁_ ×-Rel _≈₂_) (_∼₁_ ×-Rel _∼₂_)
  _×-isPreorder_ {_∼₁_ = _∼₁_} {_∼₂_ = _∼₂_} pre₁ pre₂ = record
    { isEquivalence = isEquivalence pre₁ ×-isEquivalence
                      isEquivalence pre₂
    ; reflexive     = λ {x y} 
                      _×-reflexive_  {_∼₁_ = _∼₁_} {_∼₂_ = _∼₂_}
                                     (reflexive pre₁) (reflexive pre₂)
                                     {x} {y}
    ; trans         = λ {x y z} 
                      _×-transitive_ {_∼₁_ = _∼₁_} {_∼₂_ = _∼₂_}
                                     (trans pre₁) (trans pre₂)
                                     {x} {y} {z}
    }
    where open IsPreorder

  _×-isDecEquivalence_ :
     {_≈₁_ _≈₂_} 
    IsDecEquivalence _≈₁_  IsDecEquivalence _≈₂_ 
    IsDecEquivalence (_≈₁_ ×-Rel _≈₂_)
  eq₁ ×-isDecEquivalence eq₂ = record
    { isEquivalence = isEquivalence eq₁ ×-isEquivalence
                      isEquivalence eq₂
    ; _≟_           = _≟_ eq₁ ×-decidable _≟_ eq₂
    }
    where open IsDecEquivalence

  _×-isPartialOrder_ :
     {_≈₁_ _≤₁_ _≈₂_ _≤₂_} 
    IsPartialOrder _≈₁_ _≤₁_  IsPartialOrder _≈₂_ _≤₂_ 
    IsPartialOrder (_≈₁_ ×-Rel _≈₂_) (_≤₁_ ×-Rel _≤₂_)
  _×-isPartialOrder_ {_≤₁_ = _≤₁_} {_≤₂_ = _≤₂_} po₁ po₂ = record
    { isPreorder = isPreorder po₁ ×-isPreorder isPreorder po₂
    ; antisym    = λ {x y} 
                   _×-antisymmetric_ {_≤₁_ = _≤₁_} {_≤₂_ = _≤₂_}
                                     (antisym po₁) (antisym po₂)
                                     {x} {y}
    }
    where open IsPartialOrder

  _×-isStrictPartialOrder_ :
     {_≈₁_ _<₁_ _≈₂_ _<₂_} 
    IsStrictPartialOrder _≈₁_ _<₁_  IsStrictPartialOrder _≈₂_ _<₂_ 
    IsStrictPartialOrder (_≈₁_ ×-Rel _≈₂_) (_<₁_ ×-Rel _<₂_)
  _×-isStrictPartialOrder_ {_<₁_ = _<₁_} {_≈₂_ = _≈₂_} {_<₂_ = _<₂_}
                           spo₁ spo₂ =
    record
      { isEquivalence = isEquivalence spo₁ ×-isEquivalence
                        isEquivalence spo₂
      ; irrefl        = λ {x y} 
                        ×-irreflexive₁ {_<₁_ = _<₁_}
                                       {_≈₂_ = _≈₂_} {_<₂_ = _<₂_}
                                       (irrefl spo₁) {x} {y}
      ; trans         = λ {x y z} 
                        _×-transitive_ {_∼₁_ = _<₁_} {_∼₂_ = _<₂_}
                                       (trans spo₁) (trans spo₂)
                                       {x} {y} {z}
      ; <-resp-≈      = <-resp-≈ spo₁ ×-≈-respects₂ <-resp-≈ spo₂
      }
    where open IsStrictPartialOrder

-- "Packages" (e.g. setoids) can also be combined.

_×-preorder_ :
   {p₁ p₂ p₃ p₄} 
  Preorder p₁ p₂ _  Preorder p₃ p₄ _  Preorder _ _ _
p₁ ×-preorder p₂ = record
  { isPreorder = isPreorder p₁ ×-isPreorder isPreorder p₂
  } where open Preorder

_×-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

_×-decSetoid_ :
   {d₁ d₂ d₃ d₄}  DecSetoid d₁ d₂  DecSetoid d₃ d₄  DecSetoid _ _
s₁ ×-decSetoid s₂ = record
  { isDecEquivalence = isDecEquivalence s₁ ×-isDecEquivalence
                       isDecEquivalence s₂
  } where open DecSetoid

_×-poset_ :
   {p₁ p₂ p₃ p₄}  Poset p₁ p₂ _  Poset p₃ p₄ _  Poset _ _ _
s₁ ×-poset s₂ = record
  { isPartialOrder = isPartialOrder s₁ ×-isPartialOrder
                     isPartialOrder s₂
  } where open Poset

_×-strictPartialOrder_ :
   {s₁ s₂ s₃ s₄} 
  StrictPartialOrder s₁ s₂ _  StrictPartialOrder s₃ s₄ _ 
  StrictPartialOrder _ _ _
s₁ ×-strictPartialOrder s₂ = record
  { isStrictPartialOrder = isStrictPartialOrder s₁
                             ×-isStrictPartialOrder
                           isStrictPartialOrder s₂
  } where open StrictPartialOrder

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

private

  to-cong :  {a b} {A : Set a} {B : Set b} 
            (_≡_ ×-Rel _≡_)  _≡_ {A = A × B}
  to-cong {i = (x , y)} {j = (.x , .y)} (P.refl , P.refl) = P.refl

  from-cong :  {a b} {A : Set a} {B : Set b} 
              _≡_ {A = A × B}  (_≡_ ×-Rel _≡_)
  from-cong P.refl = (P.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 , 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₂) p₁ p₂ = Dec.map′ to-cong from-cong (p₁  p₂)
  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 = Prod.map (_⟨$⟩_ f) (_⟨$⟩_ g)

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

_×-equivalence_ :
   {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
    {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
    {C : Setoid c₁ c₂} {D : Setoid d₁ d₂} 
  Equivalence A B  Equivalence C D 
  Equivalence (A ×-setoid C) (B ×-setoid D)
_×-equivalence_ {A = A} {B} {C} {D} A⇔B 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↔≡ {A = B} {B = D}) ⟨∘⟩
  (A⇔B ×-equivalence C⇔D) ⟨∘⟩
  Eq.sym (Inverse.equivalence (×-Rel↔≡ {A = A} {B = 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)
A↣B ×-injection C↣D = record
  { to        = to A↣B ×-⟶ to C↣D
  ; injective = Prod.map (injective A↣B) (injective C↣D)
  } where open Injection

_×-↣_ :  {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↔≡ {A = B} {B = D}) ⟨∘⟩
  (A↣B ×-injection C↣D) ⟨∘⟩
  Inverse.injection (Inv.sym (×-Rel↔≡ {A = A} {B = 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
  }
  where
  open LeftInverse
  eq = LeftInverse.equivalence A↞B ×-equivalence
       LeftInverse.equivalence C↞D

  left : Equivalence.from eq LeftInverseOf Equivalence.to eq
  left (x , y) = ( left-inverse-of A↞B x
                 , left-inverse-of C↞D 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.left-inverse (×-Rel↔≡ {A = B} {B = D}) ⟨∘⟩
  (A↞B ×-left-inverse C↞D) ⟨∘⟩
  Inverse.left-inverse (Inv.sym (×-Rel↔≡ {A = A} {B = 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↔≡ {A = B} {B = D}) ⟨∘⟩
  (A↠B ×-surjection C↠D) ⟨∘⟩
  Inverse.surjection (Inv.sym (×-Rel↔≡ {A = A} {B = 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↔≡ {A = B} {B = D} ⟨∘⟩
  (A↔B ×-inverse C↔D) ⟨∘⟩
  Inv.sym (×-Rel↔≡ {A = A} {B = 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}         = λ f g       Prod.map        f         g
_×-cong_ {reverse-implication} = λ f g  lam (Prod.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}           = _×-↔_