------------------------------------------------------------------------
-- The Agda standard library
--
-- Non-dependent product combinators for setoid equality preserving
-- functions
------------------------------------------------------------------------

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

module Data.Product.Function.NonDependent.Setoid where

open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Relation.Binary
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)

------------------------------------------------------------------------
-- Combinators for equality preserving functions

module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
          {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
          {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
          where

  _×-⟶_ : (A  B)  (C  D)  (A ×ₛ C)  (B ×ₛ D)
  _×-⟶_ f g = record
    { _⟨$⟩_ = fg
    ; cong  = fg-cong
    }
    where
    open Setoid (A ×ₛ C) using () renaming (_≈_ to _≈AC_)
    open Setoid (B ×ₛ D) using () renaming (_≈_ to _≈BD_)

    fg = map (f ⟨$⟩_) (g ⟨$⟩_)

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

module _ {a₁ a₂ b₁ b₂ c₁ c₂}
         {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} {C : Setoid c₁ c₂}
         where

  <_,_>ₛ : (A  B)  (A  C)  A  (B ×ₛ C)
  < f , g >ₛ = record
    { _⟨$⟩_ = < f ⟨$⟩_ , g ⟨$⟩_ >
    ; cong = < F.cong f , F.cong g >
    }

module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} where

  proj₁ₛ : (A ×ₛ B)  A
  proj₁ₛ = record { _⟨$⟩_ = proj₁ ; cong = proj₁ }

  proj₂ₛ : (A ×ₛ B)  B
  proj₂ₛ = record { _⟨$⟩_ = proj₂ ; cong = proj₂ }

  swapₛ : (A ×ₛ B)  (B ×ₛ A)
  swapₛ = < proj₂ₛ , proj₁ₛ >ₛ

------------------------------------------------------------------------
-- Combinators for more complex function types

module _  {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
          {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
          {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
          where

  _×-equivalence_ : Equivalence A B  Equivalence C D 
                    Equivalence (A ×ₛ C) (B ×ₛ D)
  _×-equivalence_ A⇔B C⇔D = record
    { to   = to   A⇔B ×-⟶ to   C⇔D
    ; from = from A⇔B ×-⟶ from C⇔D
    } where open Equivalence

  _×-injection_ : Injection A B  Injection C D 
                  Injection (A ×ₛ C) (B ×ₛ D)
  A↣B ×-injection C↣D = record
    { to        = to A↣B ×-⟶ to C↣D
    ; injective = map (injective A↣B) (injective C↣D)
    } where open Injection

  _×-left-inverse_ : LeftInverse A B  LeftInverse C D 
                     LeftInverse (A ×ₛ C) (B ×ₛ 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)

module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
  {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
  {C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
  where

  _×-surjection_ : Surjection A B  Surjection C D 
                   Surjection (A ×ₛ C) (B ×ₛ 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

  _×-inverse_ : Inverse A B  Inverse C D 
                Inverse (A ×ₛ C) (B ×ₛ 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