{-# OPTIONS --cubical-compatible --safe #-}
module Function.Construct.Composition where
open import Data.Product.Base as Product using (_,_)
open import Function.Base using (_∘_; flip)
open import Function.Bundles
open import Function.Definitions
using (Congruent; Injective; Surjective; Bijective; Inverseˡ; Inverseʳ
; Inverseᵇ)
open import Function.Structures
using (IsCongruent; IsInjection; IsSurjection ; IsBijection; IsLeftInverse
; IsRightInverse; IsInverse)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Transitive)
private
variable
a b c ℓ₁ ℓ₂ ℓ₃ : Level
A B C : Set a
module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
{f : A → B} {g : B → C}
where
congruent : Congruent ≈₁ ≈₂ f → Congruent ≈₂ ≈₃ g →
Congruent ≈₁ ≈₃ (g ∘ f)
congruent f-cong g-cong = g-cong ∘ f-cong
injective : Injective ≈₁ ≈₂ f → Injective ≈₂ ≈₃ g →
Injective ≈₁ ≈₃ (g ∘ f)
injective f-inj g-inj = f-inj ∘ g-inj
surjective : Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
Surjective ≈₁ ≈₃ (g ∘ f)
surjective f-sur g-sur x with g-sur x
... | y , gproof with f-sur y
... | z , fproof = z , gproof ∘ fproof
bijective : Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
Bijective ≈₁ ≈₃ (g ∘ f)
bijective = Product.zip′ injective surjective
module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
{f : A → B} {f⁻¹ : B → A} {g : B → C} {g⁻¹ : C → B}
where
inverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
inverseˡ f-inv g-inv = g-inv ∘ f-inv
inverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
inverseʳ f-inv g-inv = f-inv ∘ g-inv
inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
inverseᵇ = Product.zip′ inverseˡ inverseʳ
module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
{f : A → B} {g : B → C}
where
isCongruent : IsCongruent ≈₁ ≈₂ f → IsCongruent ≈₂ ≈₃ g →
IsCongruent ≈₁ ≈₃ (g ∘ f)
isCongruent f-cong g-cong = record
{ cong = G.cong ∘ F.cong
; isEquivalence₁ = F.isEquivalence₁
; isEquivalence₂ = G.isEquivalence₂
} where module F = IsCongruent f-cong; module G = IsCongruent g-cong
isInjection : IsInjection ≈₁ ≈₂ f → IsInjection ≈₂ ≈₃ g →
IsInjection ≈₁ ≈₃ (g ∘ f)
isInjection f-inj g-inj = record
{ isCongruent = isCongruent F.isCongruent G.isCongruent
; injective = injective ≈₁ ≈₂ ≈₃ F.injective G.injective
} where module F = IsInjection f-inj; module G = IsInjection g-inj
isSurjection : IsSurjection ≈₁ ≈₂ f → IsSurjection ≈₂ ≈₃ g →
IsSurjection ≈₁ ≈₃ (g ∘ f)
isSurjection f-surj g-surj = record
{ isCongruent = isCongruent F.isCongruent G.isCongruent
; surjective = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective
} where module F = IsSurjection f-surj; module G = IsSurjection g-surj
isBijection : IsBijection ≈₁ ≈₂ f → IsBijection ≈₂ ≈₃ g →
IsBijection ≈₁ ≈₃ (g ∘ f)
isBijection f-bij g-bij = record
{ isInjection = isInjection F.isInjection G.isInjection
; surjective = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective
} where module F = IsBijection f-bij; module G = IsBijection g-bij
module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
{f : A → B} {g : B → C} {f⁻¹ : B → A} {g⁻¹ : C → B}
where
isLeftInverse : IsLeftInverse ≈₁ ≈₂ f f⁻¹ → IsLeftInverse ≈₂ ≈₃ g g⁻¹ →
IsLeftInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
isLeftInverse f-invˡ g-invˡ = record
{ isCongruent = isCongruent F.isCongruent G.isCongruent
; from-cong = congruent ≈₃ ≈₂ ≈₁ G.from-cong F.from-cong
; inverseˡ = inverseˡ ≈₁ ≈₂ ≈₃ F.inverseˡ G.inverseˡ
} where module F = IsLeftInverse f-invˡ; module G = IsLeftInverse g-invˡ
isRightInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₃ g g⁻¹ →
IsRightInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
isRightInverse f-invʳ g-invʳ = record
{ isCongruent = isCongruent F.isCongruent G.isCongruent
; from-cong = congruent ≈₃ ≈₂ ≈₁ G.from-cong F.from-cong
; inverseʳ = inverseʳ ≈₁ ≈₂ ≈₃ F.inverseʳ G.inverseʳ
} where module F = IsRightInverse f-invʳ; module G = IsRightInverse g-invʳ
isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₃ g g⁻¹ →
IsInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
isInverse f-inv g-inv = record
{ isLeftInverse = isLeftInverse F.isLeftInverse G.isLeftInverse
; inverseʳ = inverseʳ ≈₁ ≈₂ ≈₃ F.inverseʳ G.inverseʳ
} where module F = IsInverse f-inv; module G = IsInverse g-inv
module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
open Setoid renaming (_≈_ to ≈)
function : Func R S → Func S T → Func R T
function f g = record
{ to = G.to ∘ F.to
; cong = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
} where module F = Func f; module G = Func g
injection : Injection R S → Injection S T → Injection R T
injection inj₁ inj₂ = record
{ to = G.to ∘ F.to
; cong = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
; injective = injective (≈ R) (≈ S) (≈ T) F.injective G.injective
} where module F = Injection inj₁; module G = Injection inj₂
surjection : Surjection R S → Surjection S T → Surjection R T
surjection surj₁ surj₂ = record
{ to = G.to ∘ F.to
; cong = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
; surjective = surjective (≈ R) (≈ S) (≈ T) F.surjective G.surjective
} where module F = Surjection surj₁; module G = Surjection surj₂
bijection : Bijection R S → Bijection S T → Bijection R T
bijection bij₁ bij₂ = record
{ to = G.to ∘ F.to
; cong = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
; bijective = bijective (≈ R) (≈ S) (≈ T) F.bijective G.bijective
} where module F = Bijection bij₁; module G = Bijection bij₂
equivalence : Equivalence R S → Equivalence S T → Equivalence R T
equivalence equiv₁ equiv₂ = record
{ to = G.to ∘ F.to
; from = F.from ∘ G.from
; to-cong = congruent (≈ R) (≈ S) (≈ T) F.to-cong G.to-cong
; from-cong = congruent (≈ T) (≈ S) (≈ R) G.from-cong F.from-cong
} where module F = Equivalence equiv₁; module G = Equivalence equiv₂
leftInverse : LeftInverse R S → LeftInverse S T → LeftInverse R T
leftInverse invˡ₁ invˡ₂ = record
{ to = G.to ∘ F.to
; from = F.from ∘ G.from
; to-cong = congruent (≈ R) (≈ S) (≈ T) F.to-cong G.to-cong
; from-cong = congruent (≈ T) (≈ S) (≈ R) G.from-cong F.from-cong
; inverseˡ = inverseˡ (≈ R) (≈ S) (≈ T) F.inverseˡ G.inverseˡ
} where module F = LeftInverse invˡ₁; module G = LeftInverse invˡ₂
rightInverse : RightInverse R S → RightInverse S T → RightInverse R T
rightInverse invʳ₁ invʳ₂ = record
{ to = G.to ∘ F.to
; from = F.from ∘ G.from
; to-cong = congruent (≈ R) (≈ S) (≈ T) F.to-cong G.to-cong
; from-cong = congruent (≈ T) (≈ S) (≈ R) G.from-cong F.from-cong
; inverseʳ = inverseʳ (≈ R) (≈ S) (≈ T) F.inverseʳ G.inverseʳ
} where module F = RightInverse invʳ₁; module G = RightInverse invʳ₂
inverse : Inverse R S → Inverse S T → Inverse R T
inverse inv₁ inv₂ = record
{ to = G.to ∘ F.to
; from = F.from ∘ G.from
; to-cong = congruent (≈ R) (≈ S) (≈ T) F.to-cong G.to-cong
; from-cong = congruent (≈ T) (≈ S) (≈ R) G.from-cong F.from-cong
; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) F.inverse G.inverse
} where module F = Inverse inv₁; module G = Inverse inv₂
infix 8 _⟶-∘_ _↣-∘_ _↠-∘_ _⤖-∘_ _⇔-∘_ _↩-∘_ _↪-∘_ _↔-∘_
_⟶-∘_ : (B ⟶ C) → (A ⟶ B) → (A ⟶ C)
_⟶-∘_ = flip function
_↣-∘_ : B ↣ C → A ↣ B → A ↣ C
_↣-∘_ = flip injection
_↠-∘_ : B ↠ C → A ↠ B → A ↠ C
_↠-∘_ = flip surjection
_⤖-∘_ : B ⤖ C → A ⤖ B → A ⤖ C
_⤖-∘_ = flip bijection
_⇔-∘_ : B ⇔ C → A ⇔ B → A ⇔ C
_⇔-∘_ = flip equivalence
_↩-∘_ : B ↩ C → A ↩ B → A ↩ C
_↩-∘_ = flip leftInverse
_↪-∘_ : B ↪ C → A ↪ B → A ↪ C
_↪-∘_ = flip rightInverse
_↔-∘_ : B ↔ C → A ↔ B → A ↔ C
_↔-∘_ = flip inverse
infix 8 _∘-⟶_ _∘-↣_ _∘-↠_ _∘-⤖_ _∘-⇔_ _∘-↩_ _∘-↪_ _∘-↔_
_∘-⟶_ = _⟶-∘_
{-# WARNING_ON_USAGE _∘-⟶_
"Warning: _∘-⟶_ was deprecated in v2.0.
Please use _⟶-∘_ instead."
#-}
_∘-↣_ = _↣-∘_
{-# WARNING_ON_USAGE _∘-↣_
"Warning: _∘-↣_ was deprecated in v2.0.
Please use _↣-∘_ instead."
#-}
_∘-↠_ = _↠-∘_
{-# WARNING_ON_USAGE _∘-↠_
"Warning: _∘-↠_ was deprecated in v2.0.
Please use _↠-∘_ instead."
#-}
_∘-⤖_ = _⤖-∘_
{-# WARNING_ON_USAGE _∘-⤖_
"Warning: _∘-⤖_ was deprecated in v2.0.
Please use _⤖-∘_ instead."
#-}
_∘-⇔_ = _⇔-∘_
{-# WARNING_ON_USAGE _∘-⇔_
"Warning: _∘-⇔_ was deprecated in v2.0.
Please use _⇔-∘_ instead."
#-}
_∘-↩_ = _↩-∘_
{-# WARNING_ON_USAGE _∘-↩_
"Warning: _∘-↩_ was deprecated in v2.0.
Please use _↩-∘_ instead."
#-}
_∘-↪_ = _↪-∘_
{-# WARNING_ON_USAGE _∘-↪_
"Warning: _∘-↪_ was deprecated in v2.0.
Please use _↪-∘_ instead."
#-}
_∘-↔_ = _↔-∘_
{-# WARNING_ON_USAGE _∘-↔_
"Warning: _∘-↔_ was deprecated in v2.0.
Please use _↔-∘_ instead."
#-}