```------------------------------------------------------------------------
-- The Agda standard library
--
-- Sum combinators for setoid equality preserving functions
------------------------------------------------------------------------

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

module Data.Sum.Function.Setoid where

open import Data.Product.Base as Prod using (_,_)
open import Data.Sum.Base as Sum
open import Data.Sum.Relation.Binary.Pointwise as Pointwise
open import Relation.Binary
open import Function.Base
open import Function.Bundles
open import Function.Definitions
open import Level

private
variable
a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂ : Level
a ℓ : Level
A B C D : Set a
≈₁ ≈₂ ≈₃ ≈₄ : Rel A ℓ
S T U V : Setoid a ℓ

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

inj₁ₛ : Func S (S ⊎ₛ T)
inj₁ₛ = record { to = inj₁ ; cong = inj₁ }

inj₂ₛ : Func T (S ⊎ₛ T)
inj₂ₛ = record { to = inj₂ ; cong = inj₂ }

[_,_]ₛ : Func S U → Func T U → Func (S ⊎ₛ T) U
[ f , g ]ₛ = record
{ to   = [ to f , to g ]
; cong = λ where
(inj₁ x∼₁y) → cong f x∼₁y
(inj₂ x∼₂y) → cong g x∼₂y
} where open Func

swapₛ : Func (S ⊎ₛ T) (T ⊎ₛ S)
swapₛ = [ inj₂ₛ , inj₁ₛ ]ₛ

------------------------------------------------------------------------
-- Definitions

⊎-injective : ∀ {f g} →
Injective ≈₁ ≈₂ f →
Injective ≈₃ ≈₄ g →
Injective (Pointwise ≈₁ ≈₃) (Pointwise ≈₂ ≈₄) (Sum.map f g)
⊎-injective f-inj g-inj {inj₁ x} {inj₁ y} (inj₁ x∼₁y) = inj₁ (f-inj x∼₁y)
⊎-injective f-inj g-inj {inj₂ x} {inj₂ y} (inj₂ x∼₂y) = inj₂ (g-inj x∼₂y)

⊎-strictlySurjective : ∀ {f : A → B} {g : C → D} →
StrictlySurjective ≈₁ f →
StrictlySurjective ≈₂ g →
StrictlySurjective (Pointwise ≈₁ ≈₂) (Sum.map f g)
⊎-strictlySurjective f-sur g-sur =
[ Prod.map inj₁ inj₁ ∘ f-sur
, Prod.map inj₂ inj₂ ∘ g-sur
]

⊎-surjective : ∀ {f : A → B} {g : C → D} →
Surjective ≈₁ ≈₂ f →
Surjective ≈₃ ≈₄ g →
Surjective (Pointwise ≈₁ ≈₃) (Pointwise ≈₂ ≈₄) (Sum.map f g)
⊎-surjective f-sur g-sur =
[ Prod.map inj₁ (λ { fwd (inj₁ x) → inj₁ (fwd x)}) ∘ f-sur
, Prod.map inj₂ (λ { fwd (inj₂ y) → inj₂ (fwd y)}) ∘ g-sur
]

infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_

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

_⊎-function_ : Func S T → Func U V → Func (S ⊎ₛ U) (T ⊎ₛ V)
S→T ⊎-function U→V = record
{ to    = Sum.map (to S→T) (to U→V)
; cong  = Pointwise.map (cong S→T) (cong U→V)
} where open Func

_⊎-equivalence_ : Equivalence S T → Equivalence U V →
Equivalence (S ⊎ₛ U) (T ⊎ₛ V)
S⇔T ⊎-equivalence U⇔V = record
{ to        = Sum.map (to S⇔T) (to U⇔V)
; from      = Sum.map (from S⇔T) (from U⇔V)
; to-cong   = Pointwise.map (to-cong S⇔T) (to-cong U⇔V)
; from-cong = Pointwise.map (from-cong S⇔T) (from-cong U⇔V)
} where open Equivalence

_⊎-injection_ : Injection S T → Injection U V →
Injection (S ⊎ₛ U) (T ⊎ₛ V)
S↣T ⊎-injection U↣V = record
{ to        = Sum.map (to S↣T) (to U↣V)
; cong      = Pointwise.map (cong S↣T) (cong U↣V)
; injective = ⊎-injective (injective S↣T) (injective U↣V)
} where open Injection

infixr 1 _⊎-surjection_ _⊎-inverse_
_⊎-surjection_ : Surjection S T → Surjection U V →
Surjection (S ⊎ₛ U) (T ⊎ₛ V)
S↠T ⊎-surjection U↠V = record
{ to              = Sum.map (to S↠T) (to U↠V)
; cong            = Pointwise.map (cong S↠T) (cong U↠V)
; surjective      = ⊎-surjective (surjective S↠T) (surjective U↠V)
} where open Surjection

_⊎-bijection_ : Bijection S T → Bijection U V →
Bijection (S ⊎ₛ U) (T ⊎ₛ V)
S⤖T ⊎-bijection U⤖V = record
{ to        = Sum.map (to S⤖T) (to U⤖V)
; cong      = Pointwise.map (cong S⤖T) (cong U⤖V)
; bijective = ⊎-injective (injective S⤖T) (injective U⤖V) ,
⊎-surjective (surjective S⤖T) (surjective U⤖V)
} where open Bijection

_⊎-leftInverse_ : LeftInverse S T → LeftInverse U V →
LeftInverse (S ⊎ₛ U) (T ⊎ₛ V)
S↩T ⊎-leftInverse U↩V = record
{ to              = Sum.map (to S↩T) (to U↩V)
; from            = Sum.map (from S↩T) (from U↩V)
; to-cong         = Pointwise.map (to-cong S↩T) (to-cong U↩V)
; from-cong       = Pointwise.map (from-cong S↩T) (from-cong U↩V)
; inverseˡ        = λ { {inj₁ _} {.(inj₁ _)} (inj₁ x) → inj₁ (inverseˡ S↩T x)
; {inj₂ _} {.(inj₂ _)} (inj₂ x) → inj₂ (inverseˡ U↩V x)}
} where open LeftInverse

_⊎-rightInverse_ : RightInverse S T → RightInverse U V →
RightInverse (S ⊎ₛ U) (T ⊎ₛ V)
S↪T ⊎-rightInverse U↪V = record
{ to              = Sum.map (to S↪T) (to U↪V)
; from            = Sum.map (from S↪T) (from U↪V)
; to-cong         = Pointwise.map (to-cong S↪T) (to-cong U↪V)
; from-cong       = Pointwise.map (from-cong S↪T) (from-cong U↪V)
; inverseʳ        = λ { {inj₁ _} (inj₁ x) → inj₁ (inverseʳ S↪T x)
; {inj₂ _} (inj₂ x) → inj₂ (inverseʳ U↪V x)
}
} where open RightInverse

_⊎-inverse_ : Inverse S T → Inverse U V →
Inverse (S ⊎ₛ U) (T ⊎ₛ V)
S↔T ⊎-inverse U↔V = record
{ to        = Sum.map (to S↔T) (to U↔V)
; from      = Sum.map (from S↔T) (from U↔V)
; to-cong   = Pointwise.map (to-cong S↔T) (to-cong U↔V)
; from-cong = Pointwise.map (from-cong S↔T) (from-cong U↔V)
; inverse   = (λ { {inj₁ _} (inj₁ x) → inj₁ (inverseˡ S↔T x)
; {inj₂ _} (inj₂ x) → inj₂ (inverseˡ U↔V x)}) ,
λ { {inj₁ _} (inj₁ x) → inj₁ (inverseʳ S↔T x)
; {inj₂ _} (inj₂ x) → inj₂ (inverseʳ U↔V 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.