------------------------------------------------------------------------
-- 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.Base as Prod
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Level using (Level)
open import Relation.Binary
open import Function

private
  variable
    a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂ : Level
    a  : Level
    A B C D : Setoid a 

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

proj₁ₛ : Func (A ×ₛ B) A
proj₁ₛ = record { to = proj₁ ; cong = proj₁ }

proj₂ₛ : Func (A ×ₛ B) B
proj₂ₛ = record { to = proj₂ ; cong = proj₂ }

<_,_>ₛ : Func A B  Func A C  Func A (B ×ₛ C)
< f , g >ₛ = record
  { to   = < to   f , to   g >
  ; cong = < cong f , cong g >
  } where open Func

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

------------------------------------------------------------------------
-- Function bundles

_×-function_ : Func A B  Func C D  Func (A ×ₛ C) (B ×ₛ D)
f ×-function g = record
  { to    = Prod.map (to f) (to g)
  ; cong  = Prod.map (cong f) (cong g)
  } where open Func

infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_

_×-equivalence_ : Equivalence A B  Equivalence C D 
                  Equivalence (A ×ₛ C) (B ×ₛ D)
_×-equivalence_ f g = record
  { to        = Prod.map (to f) (to g)
  ; from      = Prod.map (from f) (from g)
  ; to-cong   = Prod.map (to-cong f) (to-cong g)
  ; from-cong = Prod.map (from-cong f) (from-cong g)
  } where open Equivalence

_×-injection_ : Injection A B  Injection C D 
                Injection (A ×ₛ C) (B ×ₛ D)
f ×-injection g = record
  { to        = Prod.map (to f) (to g)
  ; cong      = Prod.map (cong f) (cong g)
  ; injective = Prod.map (injective f) (injective g)
  } where open Injection

_×-surjection_ : Surjection A B  Surjection C D 
                 Surjection (A ×ₛ C) (B ×ₛ D)
f ×-surjection g = record
  { to         = Prod.map (to f) (to g)
  ; cong       = Prod.map (cong f) (cong g)
  ; surjective = λ y  Prod.zip _,_  ff gg x₂  (ff (proj₁ x₂)) , (gg (proj₂ x₂))) (surjective f (proj₁ y)) (surjective g (proj₂ y))
  } where open Surjection

_×-bijection_ : Bijection A B  Bijection C D 
                Bijection (A ×ₛ C) (B ×ₛ D)
f ×-bijection g = record
  { to         = Prod.map (to f) (to g)
  ; cong       = Prod.map (cong f) (cong g)
  ; bijective  = Prod.map (injective f) (injective g) ,
                 λ { (y₀ , y₁)  Prod.zip _,_  {ff gg (x₀ , x₁)  ff x₀ , gg x₁}) (surjective f y₀) (surjective g y₁)}
  } where open Bijection

_×-leftInverse_ : LeftInverse A B  LeftInverse C D 
                  LeftInverse (A ×ₛ C) (B ×ₛ D)
f ×-leftInverse g = record
  { to        = Prod.map (to f) (to g)
  ; from      = Prod.map (from f) (from g)
  ; to-cong   = Prod.map (to-cong f) (to-cong g)
  ; from-cong = Prod.map (from-cong f) (from-cong g)
  ; inverseˡ   = λ x  inverseˡ f (proj₁ x) , inverseˡ g (proj₂ x)
  } where open LeftInverse

_×-rightInverse_ : RightInverse A B  RightInverse C D 
                   RightInverse (A ×ₛ C) (B ×ₛ D)
f ×-rightInverse g = record
  { to        = Prod.map (to f) (to g)
  ; from      = Prod.map (from f) (from g)
  ; to-cong   = Prod.map (to-cong f) (to-cong g)
  ; from-cong = Prod.map (from-cong f) (from-cong g)
  ; inverseʳ   = λ x  inverseʳ f (proj₁ x) , inverseʳ g (proj₂ x)
  } where open RightInverse

infixr 2 _×-surjection_ _×-inverse_

_×-inverse_ : Inverse A B  Inverse C D 
              Inverse (A ×ₛ C) (B ×ₛ D)
f ×-inverse g = record
  { to        = Prod.map (to f) (to g)
  ; from      = Prod.map (from f) (from g)
  ; to-cong   = Prod.map (to-cong f) (to-cong g)
  ; from-cong = Prod.map (from-cong f) (from-cong g)
  ; inverse   =  x  inverseˡ f (proj₁ x) , inverseˡ g (proj₂ x)) ,
                 x  inverseʳ f (proj₁ x) , inverseʳ g (proj₂ x))
  } where open Inverse



------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

_×-left-inverse_ = _×-leftInverse_
{-# WARNING_ON_USAGE _×-left-inverse_
"Warning: _×-left-inverse_ was deprecated in v2.0.
Please use _×-leftInverse_ instead."
#-}