------------------------------------------------------------------------
-- The Agda standard library
--
-- The composition of morphisms between algebraic structures.
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Algebra.Morphism.Construct.Composition where
open import Algebra.Bundles
open import Algebra.Morphism.Bundles
open import Algebra.Morphism.Structures
open import Function.Base using (_∘_)
import Function.Construct.Composition as Func
open import Level using (Level)
open import Relation.Binary.Morphism.Construct.Composition using (isRelHomomorphism)
open import Relation.Binary.Definitions using (Transitive)
private
variable
a b c ℓ₁ ℓ₂ ℓ₃ : Level
------------------------------------------------------------------------
-- Magmas
module _ {M₁ : RawMagma a ℓ₁}
{M₂ : RawMagma b ℓ₂}
{M₃ : RawMagma c ℓ₃}
(open RawMagma)
(≈₃-trans : Transitive (_≈_ M₃))
{f : Carrier M₁ → Carrier M₂}
{g : Carrier M₂ → Carrier M₃}
where
isMagmaHomomorphism
: IsMagmaHomomorphism M₁ M₂ f
→ IsMagmaHomomorphism M₂ M₃ g
→ IsMagmaHomomorphism M₁ M₃ (g ∘ f)
isMagmaHomomorphism f-homo g-homo = record
{ isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
; homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.homo x y)) (G.homo (f x) (f y))
} where module F = IsMagmaHomomorphism f-homo; module G = IsMagmaHomomorphism g-homo
isMagmaMonomorphism
: IsMagmaMonomorphism M₁ M₂ f
→ IsMagmaMonomorphism M₂ M₃ g
→ IsMagmaMonomorphism M₁ M₃ (g ∘ f)
isMagmaMonomorphism f-mono g-mono = record
{ isMagmaHomomorphism = isMagmaHomomorphism F.isMagmaHomomorphism G.isMagmaHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsMagmaMonomorphism f-mono; module G = IsMagmaMonomorphism g-mono
isMagmaIsomorphism
: IsMagmaIsomorphism M₁ M₂ f
→ IsMagmaIsomorphism M₂ M₃ g
→ IsMagmaIsomorphism M₁ M₃ (g ∘ f)
isMagmaIsomorphism f-iso g-iso = record
{ isMagmaMonomorphism = isMagmaMonomorphism F.isMagmaMonomorphism G.isMagmaMonomorphism
; surjective = Func.surjective _ _ (_≈_ M₃) F.surjective G.surjective
} where module F = IsMagmaIsomorphism f-iso; module G = IsMagmaIsomorphism g-iso
------------------------------------------------------------------------
-- Monoids
module _ {M₁ : RawMonoid a ℓ₁}
{M₂ : RawMonoid b ℓ₂}
{M₃ : RawMonoid c ℓ₃}
(open RawMonoid)
(≈₃-trans : Transitive (_≈_ M₃))
{f : Carrier M₁ → Carrier M₂}
{g : Carrier M₂ → Carrier M₃}
where
isMonoidHomomorphism
: IsMonoidHomomorphism M₁ M₂ f
→ IsMonoidHomomorphism M₂ M₃ g
→ IsMonoidHomomorphism M₁ M₃ (g ∘ f)
isMonoidHomomorphism f-homo g-homo = record
{ isMagmaHomomorphism = isMagmaHomomorphism ≈₃-trans F.isMagmaHomomorphism G.isMagmaHomomorphism
; ε-homo = ≈₃-trans (G.⟦⟧-cong F.ε-homo) G.ε-homo
} where module F = IsMonoidHomomorphism f-homo; module G = IsMonoidHomomorphism g-homo
isMonoidMonomorphism
: IsMonoidMonomorphism M₁ M₂ f
→ IsMonoidMonomorphism M₂ M₃ g
→ IsMonoidMonomorphism M₁ M₃ (g ∘ f)
isMonoidMonomorphism f-mono g-mono = record
{ isMonoidHomomorphism = isMonoidHomomorphism F.isMonoidHomomorphism G.isMonoidHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsMonoidMonomorphism f-mono; module G = IsMonoidMonomorphism g-mono
isMonoidIsomorphism
: IsMonoidIsomorphism M₁ M₂ f
→ IsMonoidIsomorphism M₂ M₃ g
→ IsMonoidIsomorphism M₁ M₃ (g ∘ f)
isMonoidIsomorphism f-iso g-iso = record
{ isMonoidMonomorphism = isMonoidMonomorphism F.isMonoidMonomorphism G.isMonoidMonomorphism
; surjective = Func.surjective _ _(_≈_ M₃) F.surjective G.surjective
} where module F = IsMonoidIsomorphism f-iso; module G = IsMonoidIsomorphism g-iso
------------------------------------------------------------------------
-- Groups
module _ {G₁ : RawGroup a ℓ₁}
{G₂ : RawGroup b ℓ₂}
{G₃ : RawGroup c ℓ₃}
(open RawGroup)
(≈₃-trans : Transitive (_≈_ G₃))
{f : Carrier G₁ → Carrier G₂}
{g : Carrier G₂ → Carrier G₃}
where
isGroupHomomorphism
: IsGroupHomomorphism G₁ G₂ f
→ IsGroupHomomorphism G₂ G₃ g
→ IsGroupHomomorphism G₁ G₃ (g ∘ f)
isGroupHomomorphism f-homo g-homo = record
{ isMonoidHomomorphism = isMonoidHomomorphism ≈₃-trans F.isMonoidHomomorphism G.isMonoidHomomorphism
; ⁻¹-homo = λ x → ≈₃-trans (G.⟦⟧-cong (F.⁻¹-homo x)) (G.⁻¹-homo (f x))
} where module F = IsGroupHomomorphism f-homo; module G = IsGroupHomomorphism g-homo
isGroupMonomorphism
: IsGroupMonomorphism G₁ G₂ f
→ IsGroupMonomorphism G₂ G₃ g
→ IsGroupMonomorphism G₁ G₃ (g ∘ f)
isGroupMonomorphism f-mono g-mono = record
{ isGroupHomomorphism = isGroupHomomorphism F.isGroupHomomorphism G.isGroupHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsGroupMonomorphism f-mono; module G = IsGroupMonomorphism g-mono
isGroupIsomorphism
: IsGroupIsomorphism G₁ G₂ f
→ IsGroupIsomorphism G₂ G₃ g
→ IsGroupIsomorphism G₁ G₃ (g ∘ f)
isGroupIsomorphism f-iso g-iso = record
{ isGroupMonomorphism = isGroupMonomorphism F.isGroupMonomorphism G.isGroupMonomorphism
; surjective = Func.surjective _ _ (_≈_ G₃) F.surjective G.surjective
} where module F = IsGroupIsomorphism f-iso; module G = IsGroupIsomorphism g-iso
------------------------------------------------------------------------
-- Near semirings
module _ {R₁ : RawNearSemiring a ℓ₁}
{R₂ : RawNearSemiring b ℓ₂}
{R₃ : RawNearSemiring c ℓ₃}
(open RawNearSemiring)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isNearSemiringHomomorphism
: IsNearSemiringHomomorphism R₁ R₂ f
→ IsNearSemiringHomomorphism R₂ R₃ g
→ IsNearSemiringHomomorphism R₁ R₃ (g ∘ f)
isNearSemiringHomomorphism f-homo g-homo = record
{ +-isMonoidHomomorphism = isMonoidHomomorphism ≈₃-trans F.+-isMonoidHomomorphism G.+-isMonoidHomomorphism
; *-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.*-homo x y)) (G.*-homo (f x) (f y))
} where module F = IsNearSemiringHomomorphism f-homo; module G = IsNearSemiringHomomorphism g-homo
isNearSemiringMonomorphism
: IsNearSemiringMonomorphism R₁ R₂ f
→ IsNearSemiringMonomorphism R₂ R₃ g
→ IsNearSemiringMonomorphism R₁ R₃ (g ∘ f)
isNearSemiringMonomorphism f-mono g-mono = record
{ isNearSemiringHomomorphism = isNearSemiringHomomorphism F.isNearSemiringHomomorphism G.isNearSemiringHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsNearSemiringMonomorphism f-mono; module G = IsNearSemiringMonomorphism g-mono
isNearSemiringIsomorphism
: IsNearSemiringIsomorphism R₁ R₂ f
→ IsNearSemiringIsomorphism R₂ R₃ g
→ IsNearSemiringIsomorphism R₁ R₃ (g ∘ f)
isNearSemiringIsomorphism f-iso g-iso = record
{ isNearSemiringMonomorphism = isNearSemiringMonomorphism F.isNearSemiringMonomorphism G.isNearSemiringMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsNearSemiringIsomorphism f-iso; module G = IsNearSemiringIsomorphism g-iso
------------------------------------------------------------------------
-- Semirings
module _
{R₁ : RawSemiring a ℓ₁}
{R₂ : RawSemiring b ℓ₂}
{R₃ : RawSemiring c ℓ₃}
(open RawSemiring)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isSemiringHomomorphism
: IsSemiringHomomorphism R₁ R₂ f
→ IsSemiringHomomorphism R₂ R₃ g
→ IsSemiringHomomorphism R₁ R₃ (g ∘ f)
isSemiringHomomorphism f-homo g-homo = record
{ isNearSemiringHomomorphism = isNearSemiringHomomorphism ≈₃-trans F.isNearSemiringHomomorphism G.isNearSemiringHomomorphism
; 1#-homo = ≈₃-trans (G.⟦⟧-cong F.1#-homo) G.1#-homo
} where module F = IsSemiringHomomorphism f-homo; module G = IsSemiringHomomorphism g-homo
isSemiringMonomorphism
: IsSemiringMonomorphism R₁ R₂ f
→ IsSemiringMonomorphism R₂ R₃ g
→ IsSemiringMonomorphism R₁ R₃ (g ∘ f)
isSemiringMonomorphism f-mono g-mono = record
{ isSemiringHomomorphism = isSemiringHomomorphism F.isSemiringHomomorphism G.isSemiringHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsSemiringMonomorphism f-mono; module G = IsSemiringMonomorphism g-mono
isSemiringIsomorphism
: IsSemiringIsomorphism R₁ R₂ f
→ IsSemiringIsomorphism R₂ R₃ g
→ IsSemiringIsomorphism R₁ R₃ (g ∘ f)
isSemiringIsomorphism f-iso g-iso = record
{ isSemiringMonomorphism = isSemiringMonomorphism F.isSemiringMonomorphism G.isSemiringMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsSemiringIsomorphism f-iso; module G = IsSemiringIsomorphism g-iso
------------------------------------------------------------------------
-- RingWithoutOne
module _ {R₁ : RawRingWithoutOne a ℓ₁}
{R₂ : RawRingWithoutOne b ℓ₂}
{R₃ : RawRingWithoutOne c ℓ₃}
(open RawRingWithoutOne)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isRingWithoutOneHomomorphism
: IsRingWithoutOneHomomorphism R₁ R₂ f
→ IsRingWithoutOneHomomorphism R₂ R₃ g
→ IsRingWithoutOneHomomorphism R₁ R₃ (g ∘ f)
isRingWithoutOneHomomorphism f-homo g-homo = record
{ +-isGroupHomomorphism = isGroupHomomorphism ≈₃-trans F.+-isGroupHomomorphism G.+-isGroupHomomorphism
; *-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.*-homo x y)) (G.*-homo (f x) (f y))
} where module F = IsRingWithoutOneHomomorphism f-homo; module G = IsRingWithoutOneHomomorphism g-homo
isRingWithoutOneMonomorphism
: IsRingWithoutOneMonomorphism R₁ R₂ f
→ IsRingWithoutOneMonomorphism R₂ R₃ g
→ IsRingWithoutOneMonomorphism R₁ R₃ (g ∘ f)
isRingWithoutOneMonomorphism f-mono g-mono = record
{ isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism F.isRingWithoutOneHomomorphism G.isRingWithoutOneHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsRingWithoutOneMonomorphism f-mono; module G = IsRingWithoutOneMonomorphism g-mono
isRingWithoutOneIsoMorphism
: IsRingWithoutOneIsoMorphism R₁ R₂ f
→ IsRingWithoutOneIsoMorphism R₂ R₃ g
→ IsRingWithoutOneIsoMorphism R₁ R₃ (g ∘ f)
isRingWithoutOneIsoMorphism f-iso g-iso = record
{ isRingWithoutOneMonomorphism = isRingWithoutOneMonomorphism F.isRingWithoutOneMonomorphism G.isRingWithoutOneMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsRingWithoutOneIsoMorphism f-iso; module G = IsRingWithoutOneIsoMorphism g-iso
------------------------------------------------------------------------
-- Rings
module _ {R₁ : RawRing a ℓ₁}
{R₂ : RawRing b ℓ₂}
{R₃ : RawRing c ℓ₃}
(open RawRing)
(≈₃-trans : Transitive (_≈_ R₃))
{f : Carrier R₁ → Carrier R₂}
{g : Carrier R₂ → Carrier R₃}
where
isRingHomomorphism
: IsRingHomomorphism R₁ R₂ f
→ IsRingHomomorphism R₂ R₃ g
→ IsRingHomomorphism R₁ R₃ (g ∘ f)
isRingHomomorphism f-homo g-homo = record
{ isSemiringHomomorphism = isSemiringHomomorphism ≈₃-trans F.isSemiringHomomorphism G.isSemiringHomomorphism
; -‿homo = λ x → ≈₃-trans (G.⟦⟧-cong (F.-‿homo x)) (G.-‿homo (f x))
} where module F = IsRingHomomorphism f-homo; module G = IsRingHomomorphism g-homo
isRingMonomorphism
: IsRingMonomorphism R₁ R₂ f
→ IsRingMonomorphism R₂ R₃ g
→ IsRingMonomorphism R₁ R₃ (g ∘ f)
isRingMonomorphism f-mono g-mono = record
{ isRingHomomorphism = isRingHomomorphism F.isRingHomomorphism G.isRingHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsRingMonomorphism f-mono; module G = IsRingMonomorphism g-mono
isRingIsomorphism
: IsRingIsomorphism R₁ R₂ f
→ IsRingIsomorphism R₂ R₃ g
→ IsRingIsomorphism R₁ R₃ (g ∘ f)
isRingIsomorphism f-iso g-iso = record
{ isRingMonomorphism = isRingMonomorphism F.isRingMonomorphism G.isRingMonomorphism
; surjective = Func.surjective _ _ (_≈_ R₃) F.surjective G.surjective
} where module F = IsRingIsomorphism f-iso; module G = IsRingIsomorphism g-iso
------------------------------------------------------------------------
-- Quasigroup
module _ {Q₁ : RawQuasigroup a ℓ₁}
{Q₂ : RawQuasigroup b ℓ₂}
{Q₃ : RawQuasigroup c ℓ₃}
(open RawQuasigroup)
(≈₃-trans : Transitive (_≈_ Q₃))
{f : Carrier Q₁ → Carrier Q₂}
{g : Carrier Q₂ → Carrier Q₃}
where
isQuasigroupHomomorphism
: IsQuasigroupHomomorphism Q₁ Q₂ f
→ IsQuasigroupHomomorphism Q₂ Q₃ g
→ IsQuasigroupHomomorphism Q₁ Q₃ (g ∘ f)
isQuasigroupHomomorphism f-homo g-homo = record
{ isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
; ∙-homo = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.∙-homo x y )) ( G.∙-homo (f x) (f y) )
; \\-homo = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.\\-homo x y )) ( G.\\-homo (f x) (f y) )
; //-homo = λ x y → ≈₃-trans (G.⟦⟧-cong ( F.//-homo x y )) ( G.//-homo (f x) (f y) )
} where module F = IsQuasigroupHomomorphism f-homo; module G = IsQuasigroupHomomorphism g-homo
isQuasigroupMonomorphism
: IsQuasigroupMonomorphism Q₁ Q₂ f
→ IsQuasigroupMonomorphism Q₂ Q₃ g
→ IsQuasigroupMonomorphism Q₁ Q₃ (g ∘ f)
isQuasigroupMonomorphism f-mono g-mono = record
{ isQuasigroupHomomorphism = isQuasigroupHomomorphism F.isQuasigroupHomomorphism G.isQuasigroupHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsQuasigroupMonomorphism f-mono; module G = IsQuasigroupMonomorphism g-mono
isQuasigroupIsomorphism
: IsQuasigroupIsomorphism Q₁ Q₂ f
→ IsQuasigroupIsomorphism Q₂ Q₃ g
→ IsQuasigroupIsomorphism Q₁ Q₃ (g ∘ f)
isQuasigroupIsomorphism f-iso g-iso = record
{ isQuasigroupMonomorphism = isQuasigroupMonomorphism F.isQuasigroupMonomorphism G.isQuasigroupMonomorphism
; surjective = Func.surjective _ _ (_≈_ Q₃) F.surjective G.surjective
} where module F = IsQuasigroupIsomorphism f-iso; module G = IsQuasigroupIsomorphism g-iso
------------------------------------------------------------------------
-- Loop
module _ {L₁ : RawLoop a ℓ₁}
{L₂ : RawLoop b ℓ₂}
{L₃ : RawLoop c ℓ₃}
(open RawLoop)
(≈₃-trans : Transitive (_≈_ L₃))
{f : Carrier L₁ → Carrier L₂}
{g : Carrier L₂ → Carrier L₃}
where
isLoopHomomorphism
: IsLoopHomomorphism L₁ L₂ f
→ IsLoopHomomorphism L₂ L₃ g
→ IsLoopHomomorphism L₁ L₃ (g ∘ f)
isLoopHomomorphism f-homo g-homo = record
{ isQuasigroupHomomorphism = isQuasigroupHomomorphism ≈₃-trans F.isQuasigroupHomomorphism G.isQuasigroupHomomorphism
; ε-homo = ≈₃-trans (G.⟦⟧-cong F.ε-homo) G.ε-homo
} where module F = IsLoopHomomorphism f-homo; module G = IsLoopHomomorphism g-homo
isLoopMonomorphism
: IsLoopMonomorphism L₁ L₂ f
→ IsLoopMonomorphism L₂ L₃ g
→ IsLoopMonomorphism L₁ L₃ (g ∘ f)
isLoopMonomorphism f-mono g-mono = record
{ isLoopHomomorphism = isLoopHomomorphism F.isLoopHomomorphism G.isLoopHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsLoopMonomorphism f-mono; module G = IsLoopMonomorphism g-mono
isLoopIsomorphism
: IsLoopIsomorphism L₁ L₂ f
→ IsLoopIsomorphism L₂ L₃ g
→ IsLoopIsomorphism L₁ L₃ (g ∘ f)
isLoopIsomorphism f-iso g-iso = record
{ isLoopMonomorphism = isLoopMonomorphism F.isLoopMonomorphism G.isLoopMonomorphism
; surjective = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective
} where module F = IsLoopIsomorphism f-iso; module G = IsLoopIsomorphism g-iso
------------------------------------------------------------------------
-- KleeneAlgebra
module _ {K₁ : RawKleeneAlgebra a ℓ₁}
{K₂ : RawKleeneAlgebra b ℓ₂}
{K₃ : RawKleeneAlgebra c ℓ₃}
(open RawKleeneAlgebra)
(≈₃-trans : Transitive (_≈_ K₃))
{f : Carrier K₁ → Carrier K₂}
{g : Carrier K₂ → Carrier K₃}
where
isKleeneAlgebraHomomorphism
: IsKleeneAlgebraHomomorphism K₁ K₂ f
→ IsKleeneAlgebraHomomorphism K₂ K₃ g
→ IsKleeneAlgebraHomomorphism K₁ K₃ (g ∘ f)
isKleeneAlgebraHomomorphism f-homo g-homo = record
{ isSemiringHomomorphism = isSemiringHomomorphism ≈₃-trans F.isSemiringHomomorphism G.isSemiringHomomorphism
; ⋆-homo = λ x → ≈₃-trans (G.⟦⟧-cong (F.⋆-homo x)) (G.⋆-homo (f x))
} where module F = IsKleeneAlgebraHomomorphism f-homo; module G = IsKleeneAlgebraHomomorphism g-homo
isKleeneAlgebraMonomorphism
: IsKleeneAlgebraMonomorphism K₁ K₂ f
→ IsKleeneAlgebraMonomorphism K₂ K₃ g
→ IsKleeneAlgebraMonomorphism K₁ K₃ (g ∘ f)
isKleeneAlgebraMonomorphism f-mono g-mono = record
{ isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism F.isKleeneAlgebraHomomorphism G.isKleeneAlgebraHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsKleeneAlgebraMonomorphism f-mono; module G = IsKleeneAlgebraMonomorphism g-mono
isKleeneAlgebraIsomorphism
: IsKleeneAlgebraIsomorphism K₁ K₂ f
→ IsKleeneAlgebraIsomorphism K₂ K₃ g
→ IsKleeneAlgebraIsomorphism K₁ K₃ (g ∘ f)
isKleeneAlgebraIsomorphism f-iso g-iso = record
{ isKleeneAlgebraMonomorphism = isKleeneAlgebraMonomorphism F.isKleeneAlgebraMonomorphism G.isKleeneAlgebraMonomorphism
; surjective = Func.surjective (_≈_ K₁) (_≈_ K₂) (_≈_ K₃) F.surjective G.surjective
} where module F = IsKleeneAlgebraIsomorphism f-iso; module G = IsKleeneAlgebraIsomorphism g-iso
-----------------------------------------------------------------------
-- Bundled morphisms between algebras
------------------------------------------------------------------------
-- Magma
module _ {M₁ : Magma a ℓ₁} {M₂ : Magma b ℓ₂} {M₃ : Magma c ℓ₃} where
private
module M₁ = Magma M₁
module M₂ = Magma M₂
module M₃ = Magma M₃
magmaHomomorphism : (h : MagmaHomomorphism M₁.rawMagma M₂.rawMagma) →
(k : MagmaHomomorphism M₂.rawMagma M₃.rawMagma) →
MagmaHomomorphism M₁.rawMagma M₃.rawMagma
magmaHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isMagmaHomomorphism = isMagmaHomomorphism M₃.trans H.isMagmaHomomorphism K.isMagmaHomomorphism
}
where
module H = MagmaHomomorphism h
module K = MagmaHomomorphism k
-- Monoid
module _ {M₁ : Monoid a ℓ₁} {M₂ : Monoid b ℓ₂} {M₃ : Monoid c ℓ₃} where
private
module M₁ = Monoid M₁
module M₂ = Monoid M₂
module M₃ = Monoid M₃
monoidHomomorphism : (h : MonoidHomomorphism M₁.rawMonoid M₂.rawMonoid) →
(k : MonoidHomomorphism M₂.rawMonoid M₃.rawMonoid) →
MonoidHomomorphism M₁.rawMonoid M₃.rawMonoid
monoidHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isMonoidHomomorphism = isMonoidHomomorphism M₃.trans H.isMonoidHomomorphism K.isMonoidHomomorphism
}
where
module H = MonoidHomomorphism h
module K = MonoidHomomorphism k
-- Group
module _ {M₁ : Group a ℓ₁} {M₂ : Group b ℓ₂} {M₃ : Group c ℓ₃} where
private
module M₁ = Group M₁
module M₂ = Group M₂
module M₃ = Group M₃
groupHomomorphism : (h : GroupHomomorphism M₁.rawGroup M₂.rawGroup) →
(k : GroupHomomorphism M₂.rawGroup M₃.rawGroup) →
GroupHomomorphism M₁.rawGroup M₃.rawGroup
groupHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isGroupHomomorphism = isGroupHomomorphism M₃.trans H.isGroupHomomorphism K.isGroupHomomorphism
}
where
module H = GroupHomomorphism h
module K = GroupHomomorphism k
-- NearSemiring
module _ {M₁ : NearSemiring a ℓ₁} {M₂ : NearSemiring b ℓ₂} {M₃ : NearSemiring c ℓ₃} where
private
module M₁ = NearSemiring M₁
module M₂ = NearSemiring M₂
module M₃ = NearSemiring M₃
nearSemiringHomomorphism : (h : NearSemiringHomomorphism M₁.rawNearSemiring M₂.rawNearSemiring) →
(k : NearSemiringHomomorphism M₂.rawNearSemiring M₃.rawNearSemiring) →
NearSemiringHomomorphism M₁.rawNearSemiring M₃.rawNearSemiring
nearSemiringHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isNearSemiringHomomorphism = isNearSemiringHomomorphism M₃.trans H.isNearSemiringHomomorphism K.isNearSemiringHomomorphism
}
where
module H = NearSemiringHomomorphism h
module K = NearSemiringHomomorphism k
-- Semiring
module _ {M₁ : Semiring a ℓ₁} {M₂ : Semiring b ℓ₂} {M₃ : Semiring c ℓ₃} where
private
module M₁ = Semiring M₁
module M₂ = Semiring M₂
module M₃ = Semiring M₃
semiringHomomorphism : (h : SemiringHomomorphism M₁.rawSemiring M₂.rawSemiring) →
(k : SemiringHomomorphism M₂.rawSemiring M₃.rawSemiring) →
SemiringHomomorphism M₁.rawSemiring M₃.rawSemiring
semiringHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isSemiringHomomorphism = isSemiringHomomorphism M₃.trans H.isSemiringHomomorphism K.isSemiringHomomorphism
}
where
module H = SemiringHomomorphism h
module K = SemiringHomomorphism k
-- RingWithoutOne
module _ {M₁ : RingWithoutOne a ℓ₁} {M₂ : RingWithoutOne b ℓ₂} {M₃ : RingWithoutOne c ℓ₃} where
private
module M₁ = RingWithoutOne M₁
module M₂ = RingWithoutOne M₂
module M₃ = RingWithoutOne M₃
ringWithoutOneHomomorphism : (h : RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₂.rawRingWithoutOne) →
(k : RingWithoutOneHomomorphism M₂.rawRingWithoutOne M₃.rawRingWithoutOne) →
RingWithoutOneHomomorphism M₁.rawRingWithoutOne M₃.rawRingWithoutOne
ringWithoutOneHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism M₃.trans H.isRingWithoutOneHomomorphism K.isRingWithoutOneHomomorphism
}
where
module H = RingWithoutOneHomomorphism h
module K = RingWithoutOneHomomorphism k
-- Ring
module _ {M₁ : Ring a ℓ₁} {M₂ : Ring b ℓ₂} {M₃ : Ring c ℓ₃} where
private
module M₁ = Ring M₁
module M₂ = Ring M₂
module M₃ = Ring M₃
ringHomomorphism : (h : RingHomomorphism M₁.rawRing M₂.rawRing) →
(k : RingHomomorphism M₂.rawRing M₃.rawRing) →
RingHomomorphism M₁.rawRing M₃.rawRing
ringHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isRingHomomorphism = isRingHomomorphism M₃.trans H.isRingHomomorphism K.isRingHomomorphism
}
where
module H = RingHomomorphism h
module K = RingHomomorphism k
-- Quasigroup
module _ {M₁ : Quasigroup a ℓ₁} {M₂ : Quasigroup b ℓ₂} {M₃ : Quasigroup c ℓ₃} where
private
module M₁ = Quasigroup M₁
module M₂ = Quasigroup M₂
module M₃ = Quasigroup M₃
quasigroupHomomorphism : (h : QuasigroupHomomorphism M₁.rawQuasigroup M₂.rawQuasigroup) →
(k : QuasigroupHomomorphism M₂.rawQuasigroup M₃.rawQuasigroup) →
QuasigroupHomomorphism M₁.rawQuasigroup M₃.rawQuasigroup
quasigroupHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isQuasigroupHomomorphism = isQuasigroupHomomorphism M₃.trans H.isQuasigroupHomomorphism K.isQuasigroupHomomorphism
}
where
module H = QuasigroupHomomorphism h
module K = QuasigroupHomomorphism k
-- Loop
module _ {M₁ : Loop a ℓ₁} {M₂ : Loop b ℓ₂} {M₃ : Loop c ℓ₃} where
private
module M₁ = Loop M₁
module M₂ = Loop M₂
module M₃ = Loop M₃
loopHomomorphism : (h : LoopHomomorphism M₁.rawLoop M₂.rawLoop) →
(k : LoopHomomorphism M₂.rawLoop M₃.rawLoop) →
LoopHomomorphism M₁.rawLoop M₃.rawLoop
loopHomomorphism h k = record
{ ⟦_⟧ = K.⟦_⟧ ∘ H.⟦_⟧
; isLoopHomomorphism = isLoopHomomorphism M₃.trans H.isLoopHomomorphism K.isLoopHomomorphism
}
where
module H = LoopHomomorphism h
module K = LoopHomomorphism k
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4