{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Morphism.Construct.Composition where
open import Function.Base using (_∘_)
open import Function.Construct.Composition using (surjective)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
open import Relation.Binary.Definitions using (Transitive)
open import Relation.Binary.Morphism.Bundles
using (SetoidHomomorphism; SetoidMonomorphism; SetoidIsomorphism
; PreorderHomomorphism; PosetHomomorphism)
open import Relation.Binary.Morphism.Structures
using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism
; IsOrderHomomorphism; IsOrderMonomorphism; IsOrderIsomorphism)
private
variable
a b c ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level
A B C : Set a
≈₁ ≈₂ ≈₃ ∼₁ ∼₂ ∼₃ : Rel A ℓ₁
f g : A → B
isRelHomomorphism : IsRelHomomorphism ≈₁ ≈₂ f →
IsRelHomomorphism ≈₂ ≈₃ g →
IsRelHomomorphism ≈₁ ≈₃ (g ∘ f)
isRelHomomorphism m₁ m₂ = record
{ cong = G.cong ∘ F.cong
} where module F = IsRelHomomorphism m₁; module G = IsRelHomomorphism m₂
isRelMonomorphism : IsRelMonomorphism ≈₁ ≈₂ f →
IsRelMonomorphism ≈₂ ≈₃ g →
IsRelMonomorphism ≈₁ ≈₃ (g ∘ f)
isRelMonomorphism m₁ m₂ = record
{ isHomomorphism = isRelHomomorphism F.isHomomorphism G.isHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsRelMonomorphism m₁; module G = IsRelMonomorphism m₂
isRelIsomorphism : Transitive ≈₃ →
IsRelIsomorphism ≈₁ ≈₂ f →
IsRelIsomorphism ≈₂ ≈₃ g →
IsRelIsomorphism ≈₁ ≈₃ (g ∘ f)
isRelIsomorphism {≈₃ = ≈₃} ≈₃-trans m₁ m₂ = record
{ isMonomorphism = isRelMonomorphism F.isMonomorphism G.isMonomorphism
; surjective = surjective _ _ ≈₃ F.surjective G.surjective
} where module F = IsRelIsomorphism m₁; module G = IsRelIsomorphism m₂
module _ {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} {U : Setoid c ℓ₃} where
setoidHomomorphism : SetoidHomomorphism S T →
SetoidHomomorphism T U →
SetoidHomomorphism S U
setoidHomomorphism ST TU = record
{ isRelHomomorphism = isRelHomomorphism ST.isRelHomomorphism TU.isRelHomomorphism
} where module ST = SetoidHomomorphism ST; module TU = SetoidHomomorphism TU
setoidMonomorphism : SetoidMonomorphism S T →
SetoidMonomorphism T U →
SetoidMonomorphism S U
setoidMonomorphism ST TU = record
{ isRelMonomorphism = isRelMonomorphism ST.isRelMonomorphism TU.isRelMonomorphism
} where module ST = SetoidMonomorphism ST; module TU = SetoidMonomorphism TU
setoidIsomorphism : SetoidIsomorphism S T →
SetoidIsomorphism T U →
SetoidIsomorphism S U
setoidIsomorphism ST TU = record
{ isRelIsomorphism = isRelIsomorphism (Setoid.trans U) ST.isRelIsomorphism TU.isRelIsomorphism
} where module ST = SetoidIsomorphism ST; module TU = SetoidIsomorphism TU
isOrderHomomorphism : IsOrderHomomorphism ≈₁ ≈₂ ∼₁ ∼₂ f →
IsOrderHomomorphism ≈₂ ≈₃ ∼₂ ∼₃ g →
IsOrderHomomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
isOrderHomomorphism m₁ m₂ = record
{ cong = G.cong ∘ F.cong
; mono = G.mono ∘ F.mono
} where module F = IsOrderHomomorphism m₁; module G = IsOrderHomomorphism m₂
isOrderMonomorphism : IsOrderMonomorphism ≈₁ ≈₂ ∼₁ ∼₂ f →
IsOrderMonomorphism ≈₂ ≈₃ ∼₂ ∼₃ g →
IsOrderMonomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
isOrderMonomorphism m₁ m₂ = record
{ isOrderHomomorphism = isOrderHomomorphism F.isOrderHomomorphism G.isOrderHomomorphism
; injective = F.injective ∘ G.injective
; cancel = F.cancel ∘ G.cancel
} where module F = IsOrderMonomorphism m₁; module G = IsOrderMonomorphism m₂
isOrderIsomorphism : Transitive ≈₃ →
IsOrderIsomorphism ≈₁ ≈₂ ∼₁ ∼₂ f →
IsOrderIsomorphism ≈₂ ≈₃ ∼₂ ∼₃ g →
IsOrderIsomorphism ≈₁ ≈₃ ∼₁ ∼₃ (g ∘ f)
isOrderIsomorphism {≈₃ = ≈₃} ≈₃-trans m₁ m₂ = record
{ isOrderMonomorphism = isOrderMonomorphism F.isOrderMonomorphism G.isOrderMonomorphism
; surjective = surjective _ _ ≈₃ F.surjective G.surjective
} where module F = IsOrderIsomorphism m₁; module G = IsOrderIsomorphism m₂
module _ {P : Preorder a ℓ₁ ℓ₂} {Q : Preorder b ℓ₃ ℓ₄} {R : Preorder c ℓ₅ ℓ₆} where
preorderHomomorphism : PreorderHomomorphism P Q →
PreorderHomomorphism Q R →
PreorderHomomorphism P R
preorderHomomorphism PQ QR = record
{ isOrderHomomorphism = isOrderHomomorphism PQ.isOrderHomomorphism QR.isOrderHomomorphism
} where module PQ = PreorderHomomorphism PQ; module QR = PreorderHomomorphism QR
module _ {P : Poset a ℓ₁ ℓ₂} {Q : Poset b ℓ₃ ℓ₄} {R : Poset c ℓ₅ ℓ₆} where
posetHomomorphism : PosetHomomorphism P Q →
PosetHomomorphism Q R →
PosetHomomorphism P R
posetHomomorphism PQ QR = record
{ isOrderHomomorphism = isOrderHomomorphism PQ.isOrderHomomorphism QR.isOrderHomomorphism
} where module PQ = PosetHomomorphism PQ; module QR = PosetHomomorphism QR