{-# OPTIONS --cubical-compatible --safe #-}
module Data.Product.Function.NonDependent.Setoid where
open import Data.Product.Base using (map; _,_; <_,_>; proj₁; proj₂)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Relation.Binary
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
using (Injection; _↣_; module Injection)
open import Function.Inverse as Inv
using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
using (LeftInverse; _↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj
using (Surjection; _↠_; module Surjection)
module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
{A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
{C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
where
infixr 2 _×-⟶_
_×-⟶_ : (A ⟶ B) → (C ⟶ D) → (A ×ₛ C) ⟶ (B ×ₛ D)
_×-⟶_ f g = record
{ _⟨$⟩_ = fg
; cong = fg-cong
}
where
open Setoid (A ×ₛ C) using () renaming (_≈_ to _≈AC_)
open Setoid (B ×ₛ D) using () renaming (_≈_ to _≈BD_)
fg = map (f ⟨$⟩_) (g ⟨$⟩_)
fg-cong : _≈AC_ =[ fg ]⇒ _≈BD_
fg-cong (_∼₁_ , _∼₂_) = (F.cong f _∼₁_ , F.cong g _∼₂_)
module _ {a₁ a₂ b₁ b₂ c₁ c₂}
{A : Setoid a₁ a₂} {B : Setoid b₁ b₂} {C : Setoid c₁ c₂}
where
<_,_>ₛ : (A ⟶ B) → (A ⟶ C) → A ⟶ (B ×ₛ C)
< f , g >ₛ = record
{ _⟨$⟩_ = < f ⟨$⟩_ , g ⟨$⟩_ >
; cong = < F.cong f , F.cong g >
}
module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} where
proj₁ₛ : (A ×ₛ B) ⟶ A
proj₁ₛ = record { _⟨$⟩_ = proj₁ ; cong = proj₁ }
proj₂ₛ : (A ×ₛ B) ⟶ B
proj₂ₛ = record { _⟨$⟩_ = proj₂ ; cong = proj₂ }
swapₛ : (A ×ₛ B) ⟶ (B ×ₛ A)
swapₛ = < proj₂ₛ , proj₁ₛ >ₛ
module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
{A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
{C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
where
infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_
_×-equivalence_ : Equivalence A B → Equivalence C D →
Equivalence (A ×ₛ C) (B ×ₛ D)
_×-equivalence_ A⇔B C⇔D = record
{ to = to A⇔B ×-⟶ to C⇔D
; from = from A⇔B ×-⟶ from C⇔D
} where open Equivalence
_×-injection_ : Injection A B → Injection C D →
Injection (A ×ₛ C) (B ×ₛ D)
A↣B ×-injection C↣D = record
{ to = to A↣B ×-⟶ to C↣D
; injective = map (injective A↣B) (injective C↣D)
} where open Injection
_×-left-inverse_ : LeftInverse A B → LeftInverse C D →
LeftInverse (A ×ₛ C) (B ×ₛ D)
A↞B ×-left-inverse C↞D = record
{ to = Equivalence.to eq
; from = Equivalence.from eq
; left-inverse-of = left
}
where
open LeftInverse
eq = LeftInverse.equivalence A↞B ×-equivalence
LeftInverse.equivalence C↞D
left : Equivalence.from eq LeftInverseOf Equivalence.to eq
left (x , y) = (left-inverse-of A↞B x , left-inverse-of C↞D y)
module _ {a₁ a₂ b₁ b₂ c₁ c₂ d₁ d₂}
{A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
{C : Setoid c₁ c₂} {D : Setoid d₁ d₂}
where
infixr 2 _×-surjection_ _×-inverse_
_×-surjection_ : Surjection A B → Surjection C D →
Surjection (A ×ₛ C) (B ×ₛ D)
A↠B ×-surjection C↠D = record
{ to = LeftInverse.from inv
; surjective = record
{ from = LeftInverse.to inv
; right-inverse-of = LeftInverse.left-inverse-of inv
}
}
where
open Surjection
inv = right-inverse A↠B ×-left-inverse right-inverse C↠D
_×-inverse_ : Inverse A B → Inverse C D →
Inverse (A ×ₛ C) (B ×ₛ D)
A↔B ×-inverse C↔D = record
{ to = Surjection.to surj
; from = Surjection.from surj
; inverse-of = record
{ left-inverse-of = LeftInverse.left-inverse-of inv
; right-inverse-of = Surjection.right-inverse-of surj
}
}
where
open Inverse
surj = Inverse.surjection A↔B ×-surjection
Inverse.surjection C↔D
inv = Inverse.left-inverse A↔B ×-left-inverse
Inverse.left-inverse C↔D