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

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

module Data.Product.Function.NonDependent.Propositional where

open import Data.Product.Base using (_×_; map)
open import Data.Product.Function.NonDependent.Setoid
open import Data.Product.Relation.Binary.Pointwise.NonDependent
  using (_×ₛ_; Pointwise-≡↔≡)
open import Function.Base using (id)
open import Function.Bundles
  using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _⤖_; _↩_; _↪_; _↔_)
open import Function.Properties.Inverse as Inv
  using (Inverse⇒Equivalence; Inverse⇒Injection; Inverse⇒Surjection;
         Inverse⇒Bijection)
open import Function.Related.Propositional
  using (_∼[_]_; implication; reverseImplication; equivalence; injection;
         reverseInjection; leftInverse; surjection; bijection)
import Function.Construct.Composition as Compose
open import Level using (Level; _⊔_)
open import Relation.Binary hiding (_⇔_)
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 2 _×-⟶_ _×-⇔_ _×-↣_ _×-↠_ _×-⤖_ _×-↩_ _×-↪_ _×-↔_

_×-⟶_ : 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.bijection Inverse⇒Bijection _×-bijection_

_×-↩_ : 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.inverse id _×-inverse_

infixr 2 _×-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}           = _×-↔_