------------------------------------------------------------------------
-- The Agda standard library
--
-- Sum combinators for propositional equality preserving functions
------------------------------------------------------------------------

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

module Data.Sum.Function.Propositional where

open import Data.Sum.Base using (_⊎_)
open import Data.Sum.Function.Setoid
open import Data.Sum.Relation.Binary.Pointwise using (Pointwise-≡↔≡; _⊎ₛ_)
open import Function.Construct.Composition as Compose
open import Function.Related.Propositional
  using (_∼[_]_; implication; reverseImplication; equivalence; injection;
    reverseInjection; leftInverse; surjection; bijection)
open import Function.Base using (id)
open import Function.Bundles
  using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _↩_; _↪_; _⤖_; _↔_)
open import Function.Properties.Inverse as Inv
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality.Properties using (setoid)

private
  variable
    a b c d : Level
    A B C D : Set a


------------------------------------------------------------------------
-- Helper lemma

private
  liftViaInverse : {R : ∀ {a b ℓ₁ ℓ₂} → REL (Setoid a ℓ₁) (Setoid b ℓ₂) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)} →
                   (∀ {a b c ℓ₁ ℓ₂ ℓ₃} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} {U : Setoid c ℓ₃} → R S T → R T U → R S U) →
                   (∀ {a b ℓ₁ ℓ₂} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} → Inverse S T → R S T) →
                   (R (setoid A) (setoid C) → R (setoid B) (setoid D) → R (setoid A ⊎ₛ setoid B) (setoid C ⊎ₛ setoid D)) →
                   R (setoid A) (setoid C) → R (setoid B) (setoid D) →
                   R (setoid (A ⊎ B)) (setoid (C ⊎ D))
  liftViaInverse trans inv⇒R lift RAC RBD =
    Inv.transportVia trans inv⇒R (Inv.sym (Pointwise-≡↔≡ _ _)) (lift RAC RBD) (Pointwise-≡↔≡ _ _)

------------------------------------------------------------------------
-- Combinators for various function types

infixr  _⊎-⟶_ _⊎-⇔_ _⊎-↣_ _⊎-↩_ _⊎-↪_ _⊎-↔_

_⊎-⟶_ : A ⟶ B → C ⟶ D → (A ⊎ C) ⟶ (B ⊎ D)
_⊎-⟶_ = liftViaInverse Compose.function Inv.toFunction _⊎-function_


_⊎-⇔_ : A ⇔ B → C ⇔ D → (A ⊎ C) ⇔ (B ⊎ D)
_⊎-⇔_ = liftViaInverse Compose.equivalence Inverse⇒Equivalence _⊎-equivalence_

_⊎-↣_ : A ↣ B → C ↣ D → (A ⊎ C) ↣ (B ⊎ D)
_⊎-↣_ = liftViaInverse Compose.injection Inverse⇒Injection _⊎-injection_

_⊎-↠_ : A ↠ B → C ↠ D → (A ⊎ C) ↠ (B ⊎ D)
_⊎-↠_ = liftViaInverse Compose.surjection Inverse⇒Surjection _⊎-surjection_

_⊎-↩_ : A ↩ B → C ↩ D → (A ⊎ C) ↩ (B ⊎ D)
_⊎-↩_ = liftViaInverse Compose.leftInverse Inverse.leftInverse _⊎-leftInverse_

_⊎-↪_ : A ↪ B → C ↪ D → (A ⊎ C) ↪ (B ⊎ D)
_⊎-↪_ = liftViaInverse Compose.rightInverse Inverse.rightInverse _⊎-rightInverse_

_⊎-⤖_ : A ⤖ B → C ⤖ D → (A ⊎ C) ⤖ (B ⊎ D)
_⊎-⤖_ = liftViaInverse Compose.bijection Inverse⇒Bijection _⊎-bijection_

_⊎-↔_ : A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
_⊎-↔_ = liftViaInverse Compose.inverse id _⊎-inverse_

infixr  _⊎-cong_

_⊎-cong_ : ∀ {k} → A ∼[ k ] B → C ∼[ k ] D → (A ⊎ C) ∼[ k ] (B ⊎ D)
_⊎-cong_ {k = implication}         = _⊎-⟶_
_⊎-cong_ {k = reverseImplication}  = _⊎-⟶_
_⊎-cong_ {k = equivalence}         = _⊎-⇔_
_⊎-cong_ {k = injection}           = _⊎-↣_
_⊎-cong_ {k = reverseInjection}    = _⊎-↣_
_⊎-cong_ {k = leftInverse}         = _⊎-↪_
_⊎-cong_ {k = surjection}          = _⊎-↠_
_⊎-cong_ {k = bijection}           = _⊎-↔_