{-# 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
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-≡↔≡
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} = _×-↔_