```------------------------------------------------------------------------
-- The Agda standard library
--
-- Composition of functional properties
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Function.Construct.Composition where

open import Data.Product using (_,_)
open import Function
open import Level using (Level)
open import Relation.Binary as B hiding (_⇔_; IsEquivalence)

private
variable
a b c ℓ₁ ℓ₂ ℓ₃ : Level
A : Set a
B : Set b
C : Set c

------------------------------------------------------------------------
-- Properties

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 : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
Surjective ≈₁ ≈₃ (g ∘ f)
surjective trans g-cong f-sur g-sur x with g-sur x
... | y , fy≈x  with f-sur y
...   | z , fz≈y = z , trans (g-cong fz≈y) fy≈x

bijective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
Bijective ≈₁ ≈₃ (g ∘ f)
bijective trans g-cong (f-inj , f-sur) (g-inj , g-sur) =
injective f-inj g-inj , surjective trans g-cong f-sur g-sur

module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
(f : A → B) {f⁻¹ : B → A} {g : B → C} (g⁻¹ : C → B)
where

inverseˡ : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
inverseˡ trn g-cong f-inv g-inv x = trn (g-cong (f-inv _)) (g-inv x)

inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ →
Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
inverseʳ trn f⁻¹-cong f-inv g-inv x = trn (f⁻¹-cong (g-inv _)) (f-inv x)

inverseᵇ : Transitive ≈₁ → Transitive ≈₃ →
Congruent ≈₂ ≈₃ g → Congruent ≈₂ ≈₁ f⁻¹ →
Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
inverseᵇ trn₁ trn₃ g-cong f⁻¹-cong (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) =
inverseˡ trn₃ g-cong f-invˡ g-invˡ , inverseʳ trn₁ f⁻¹-cong f-invʳ g-invʳ

------------------------------------------------------------------------
-- Structures

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 ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong 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 ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong 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
; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
; inverseˡ    = inverseˡ ≈₁ ≈₂ ≈₃ f _ G.Eq₂.trans G.cong₁ 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
; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
; inverseʳ    = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ 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ʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ
} where module F = IsInverse f-inv; module G = IsInverse g-inv

------------------------------------------------------------------------
-- Setoid bundles

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
{ f    = G.f ∘ F.f
; 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
{ f         = G.f ∘ F.f
; 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
{ f          = G.f ∘ F.f
; cong       = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
; surjective = surjective (≈ R) (≈ S) (≈ T) G.Eq₂.trans G.cong 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
{ f         = G.f ∘ F.f
; cong      = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
; bijective = bijective (≈ R) (≈ S) (≈ T) (trans T) G.cong 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
{ f        = G.f ∘ F.f
; g        = F.g ∘ G.g
; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
} where module F = Equivalence equiv₁; module G = Equivalence equiv₂

leftInverse : LeftInverse R S → LeftInverse S T → LeftInverse R T
leftInverse invˡ₁ invˡ₂ = record
{ f        = G.f ∘ F.f
; g        = F.g ∘ G.g
; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
; inverseˡ = inverseˡ (≈ R) (≈ S) (≈ T) F.f _ (trans T) G.cong₁ 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
{ f        = G.f ∘ F.f
; g        = F.g ∘ G.g
; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
; inverseʳ = inverseʳ (≈ R) (≈ S) (≈ T) _ G.g (trans R) F.cong₂ 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
{ f       = G.f ∘ F.f
; f⁻¹     = F.f⁻¹ ∘ G.f⁻¹
; cong₁   = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
; cong₂   = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ (trans R) (trans T) G.cong₁ F.cong₂ F.inverse G.inverse
} where module F = Inverse inv₁; module G = Inverse inv₂

------------------------------------------------------------------------
-- Propositional bundles

infix 8 _∘-⟶_ _∘-↣_ _∘-↠_ _∘-⤖_ _∘-⇔_ _∘-↩_ _∘-↪_ _∘-↔_

_∘-⟶_ : (A ⟶ B) → (B ⟶ C) → (A ⟶ C)
_∘-⟶_ = function

_∘-↣_ : A ↣ B → B ↣ C → A ↣ C
_∘-↣_ = injection

_∘-↠_ : A ↠ B → B ↠ C → A ↠ C
_∘-↠_ = surjection

_∘-⤖_ : A ⤖ B → B ⤖ C → A ⤖ C
_∘-⤖_ = bijection

_∘-⇔_ : A ⇔ B → B ⇔ C → A ⇔ C
_∘-⇔_ = equivalence

_∘-↩_ : A ↩ B → B ↩ C → A ↩ C
_∘-↩_ = leftInverse

_∘-↪_ : A ↪ B → B ↪ C → A ↪ C
_∘-↪_ = rightInverse

_∘-↔_ : A ↔ B → B ↔ C → A ↔ C
_∘-↔_ = inverse
```