------------------------------------------------------------------------ -- The Agda standard library -- -- Morphisms between algebraic structures ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} open import Relation.Binary.Core module Algebra.Morphism.Structures where open import Algebra.Core open import Algebra.Bundles import Algebra.Morphism.Definitions as MorphismDefinitions open import Level using (Level; _⊔_) import Function.Definitions as FunctionDefinitions open import Relation.Binary.Morphism.Structures private variable a b ℓ₁ ℓ₂ : Level ------------------------------------------------------------------------ -- Morphisms over magma-like structures ------------------------------------------------------------------------ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) where open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_) open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_) open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ homo : Homomorphic₂ ⟦_⟧ _∙_ _◦_ open IsRelHomomorphism isRelHomomorphism public renaming (cong to ⟦⟧-cong) record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsMagmaHomomorphism isMagmaHomomorphism public isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧ isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = injective } record IsMagmaIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsMagmaMonomorphism isMagmaMonomorphism public isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧ isRelIsomorphism = record { isMonomorphism = isRelMonomorphism ; surjective = surjective } ------------------------------------------------------------------------ -- Morphisms over monoid-like structures ------------------------------------------------------------------------ module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) where open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁) open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂) open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ open MagmaMorphisms (RawMonoid.rawMagma M₁) (RawMonoid.rawMagma M₂) record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧ ε-homo : Homomorphic₀ ⟦_⟧ ε₁ ε₂ open IsMagmaHomomorphism isMagmaHomomorphism public record IsMonoidMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsMonoidHomomorphism isMonoidHomomorphism public isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧ isMagmaMonomorphism = record { isMagmaHomomorphism = isMagmaHomomorphism ; injective = injective } open IsMagmaMonomorphism isMagmaMonomorphism public using (isRelMonomorphism) record IsMonoidIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsMonoidMonomorphism isMonoidMonomorphism public isMagmaIsomorphism : IsMagmaIsomorphism ⟦_⟧ isMagmaIsomorphism = record { isMagmaMonomorphism = isMagmaMonomorphism ; surjective = surjective } open IsMagmaIsomorphism isMagmaIsomorphism public using (isRelIsomorphism) ------------------------------------------------------------------------ -- Morphisms over group-like structures ------------------------------------------------------------------------ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) where open RawGroup G₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁) open RawGroup G₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂) open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ open MagmaMorphisms (RawGroup.rawMagma G₁) (RawGroup.rawMagma G₂) open MonoidMorphisms (RawGroup.rawMonoid G₁) (RawGroup.rawMonoid G₂) record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ ⁻¹-homo : Homomorphic₁ ⟦_⟧ _⁻¹₁ _⁻¹₂ open IsMonoidHomomorphism isMonoidHomomorphism public record IsGroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsGroupHomomorphism isGroupHomomorphism public renaming (homo to ∙-homo) isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧ isMonoidMonomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism ; injective = injective } open IsMonoidMonomorphism isMonoidMonomorphism public using (isRelMonomorphism; isMagmaMonomorphism) record IsGroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsGroupMonomorphism isGroupMonomorphism public isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧ isMonoidIsomorphism = record { isMonoidMonomorphism = isMonoidMonomorphism ; surjective = surjective } open IsMonoidIsomorphism isMonoidIsomorphism public using (isRelIsomorphism; isMagmaIsomorphism) ------------------------------------------------------------------------ -- Morphisms over near-semiring-like structures ------------------------------------------------------------------------ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSemiring b ℓ₂) where open RawNearSemiring R₁ renaming ( Carrier to A; _≈_ to _≈₁_ ; +-rawMonoid to +-rawMonoid₁ ; _*_ to _*₁_ ; *-rawMagma to *-rawMagma₁) open RawNearSemiring R₂ renaming ( Carrier to B; _≈_ to _≈₂_ ; +-rawMonoid to +-rawMonoid₂ ; _*_ to _*₂_ ; *-rawMagma to *-rawMagma₂) private module + = MonoidMorphisms +-rawMonoid₁ +-rawMonoid₂ module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂ open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ record IsNearSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field +-isMonoidHomomorphism : +.IsMonoidHomomorphism ⟦_⟧ *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_ open +.IsMonoidHomomorphism +-isMonoidHomomorphism public renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism) *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧ *-isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism ; homo = *-homo } record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsNearSemiringHomomorphism isNearSemiringHomomorphism public +-isMonoidMonomorphism : +.IsMonoidMonomorphism ⟦_⟧ +-isMonoidMonomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism ; injective = injective } open +.IsMonoidMonomorphism +-isMonoidMonomorphism public using (isRelMonomorphism) renaming (isMagmaMonomorphism to +-isMagmaMonomorphsm) *-isMagmaMonomorphism : *.IsMagmaMonomorphism ⟦_⟧ *-isMagmaMonomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism ; injective = injective } record IsNearSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsNearSemiringMonomorphism isNearSemiringMonomorphism public +-isMonoidIsomorphism : +.IsMonoidIsomorphism ⟦_⟧ +-isMonoidIsomorphism = record { isMonoidMonomorphism = +-isMonoidMonomorphism ; surjective = surjective } open +.IsMonoidIsomorphism +-isMonoidIsomorphism public using (isRelIsomorphism) renaming (isMagmaIsomorphism to +-isMagmaIsomorphism) *-isMagmaIsomorphism : *.IsMagmaIsomorphism ⟦_⟧ *-isMagmaIsomorphism = record { isMagmaMonomorphism = *-isMagmaMonomorphism ; surjective = surjective } ------------------------------------------------------------------------ -- Morphisms over semiring-like structures ------------------------------------------------------------------------ module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ₂) where open RawSemiring R₁ renaming ( Carrier to A; _≈_ to _≈₁_ ; 1# to 1#₁ ; rawNearSemiring to rawNearSemiring₁ ; *-rawMonoid to *-rawMonoid₁) open RawSemiring R₂ renaming ( Carrier to B; _≈_ to _≈₂_ ; 1# to 1#₂ ; rawNearSemiring to rawNearSemiring₂ ; *-rawMonoid to *-rawMonoid₂) private module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂ open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ open NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂ record IsSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧ 1#-homo : Homomorphic₀ ⟦_⟧ 1#₁ 1#₂ open IsNearSemiringHomomorphism isNearSemiringHomomorphism public *-isMonoidHomomorphism : *.IsMonoidHomomorphism ⟦_⟧ *-isMonoidHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism ; ε-homo = 1#-homo } record IsSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsSemiringHomomorphism isSemiringHomomorphism public isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧ isNearSemiringMonomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism ; injective = injective } open IsNearSemiringMonomorphism isNearSemiringMonomorphism public using (+-isMonoidMonomorphism; *-isMagmaMonomorphism) *-isMonoidMonomorphism : *.IsMonoidMonomorphism ⟦_⟧ *-isMonoidMonomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism ; injective = injective } record IsSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsSemiringMonomorphism isSemiringMonomorphism public isNearSemiringIsomorphism : IsNearSemiringIsomorphism ⟦_⟧ isNearSemiringIsomorphism = record { isNearSemiringMonomorphism = isNearSemiringMonomorphism ; surjective = surjective } open IsNearSemiringIsomorphism isNearSemiringIsomorphism public using (+-isMonoidIsomorphism; *-isMagmaIsomorphism) *-isMonoidIsomorphism : *.IsMonoidIsomorphism ⟦_⟧ *-isMonoidIsomorphism = record { isMonoidMonomorphism = *-isMonoidMonomorphism ; surjective = surjective } ------------------------------------------------------------------------ -- Morphisms over ring-like structures ------------------------------------------------------------------------ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where open RawRing R₁ renaming ( Carrier to A; _≈_ to _≈₁_ ; -_ to -₁_ ; rawSemiring to rawSemiring₁ ; *-rawMonoid to *-rawMonoid₁ ; +-rawGroup to +-rawGroup₁) open RawRing R₂ renaming ( Carrier to B; _≈_ to _≈₂_ ; -_ to -₂_ ; rawSemiring to rawSemiring₂ ; *-rawMonoid to *-rawMonoid₂ ; +-rawGroup to +-rawGroup₂) module + = GroupMorphisms +-rawGroup₁ +-rawGroup₂ module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂ open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ open SemiringMorphisms rawSemiring₁ rawSemiring₂ record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧ -‿homo : Homomorphic₁ ⟦_⟧ -₁_ -₂_ open IsSemiringHomomorphism isSemiringHomomorphism public +-isGroupHomomorphism : +.IsGroupHomomorphism ⟦_⟧ +-isGroupHomomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism ; ⁻¹-homo = -‿homo } record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRingHomomorphism : IsRingHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsRingHomomorphism isRingHomomorphism public isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧ isSemiringMonomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism ; injective = injective } +-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧ +-isGroupMonomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism ; injective = injective } open +.IsGroupMonomorphism +-isGroupMonomorphism using (isRelMonomorphism) renaming ( isMagmaMonomorphism to +-isMagmaMonomorphism ; isMonoidMonomorphism to +-isMonoidMonomorphism ) *-isMonoidMonomorphism : *.IsMonoidMonomorphism ⟦_⟧ *-isMonoidMonomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism ; injective = injective } open *.IsMonoidMonomorphism *-isMonoidMonomorphism public using () renaming (isMagmaMonomorphism to *-isMagmaMonomorphism) record IsRingIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isRingMonomorphism : IsRingMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsRingMonomorphism isRingMonomorphism public isSemiringIsomorphism : IsSemiringIsomorphism ⟦_⟧ isSemiringIsomorphism = record { isSemiringMonomorphism = isSemiringMonomorphism ; surjective = surjective } +-isGroupIsomorphism : +.IsGroupIsomorphism ⟦_⟧ +-isGroupIsomorphism = record { isGroupMonomorphism = +-isGroupMonomorphism ; surjective = surjective } open +.IsGroupIsomorphism +-isGroupIsomorphism using (isRelIsomorphism) renaming ( isMagmaIsomorphism to +-isMagmaIsomorphism ; isMonoidIsomorphism to +-isMonoidIsomorphisn ) *-isMonoidIsomorphism : *.IsMonoidIsomorphism ⟦_⟧ *-isMonoidIsomorphism = record { isMonoidMonomorphism = *-isMonoidMonomorphism ; surjective = surjective } open *.IsMonoidIsomorphism *-isMonoidIsomorphism public using () renaming (isMagmaIsomorphism to *-isMagmaIsomorphisn) ------------------------------------------------------------------------ -- Morphisms over quasigroup-like structures ------------------------------------------------------------------------ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup b ℓ₂) where open RawQuasigroup Q₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁; \\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁; _≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_) open RawQuasigroup Q₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂; \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂; _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_) module ∙ = MagmaMorphisms ∙-rawMagma₁ ∙-rawMagma₂ module \\ = MagmaMorphisms \\-rawMagma₁ \\-rawMagma₂ module // = MagmaMorphisms //-rawMagma₁ //-rawMagma₂ open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ ∙-homo : Homomorphic₂ ⟦_⟧ _∙₁_ _∙₂_ \\-homo : Homomorphic₂ ⟦_⟧ _\\₁_ _\\₂_ //-homo : Homomorphic₂ ⟦_⟧ _//₁_ _//₂_ open IsRelHomomorphism isRelHomomorphism public renaming (cong to ⟦⟧-cong) ∙-isMagmaHomomorphism : ∙.IsMagmaHomomorphism ⟦_⟧ ∙-isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism ; homo = ∙-homo } \\-isMagmaHomomorphism : \\.IsMagmaHomomorphism ⟦_⟧ \\-isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism ; homo = \\-homo } //-isMagmaHomomorphism : //.IsMagmaHomomorphism ⟦_⟧ //-isMagmaHomomorphism = record { isRelHomomorphism = isRelHomomorphism ; homo = //-homo } record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsQuasigroupHomomorphism isQuasigroupHomomorphism public ∙-isMagmaMonomorphism : ∙.IsMagmaMonomorphism ⟦_⟧ ∙-isMagmaMonomorphism = record { isMagmaHomomorphism = ∙-isMagmaHomomorphism ; injective = injective } \\-isMagmaMonomorphism : \\.IsMagmaMonomorphism ⟦_⟧ \\-isMagmaMonomorphism = record { isMagmaHomomorphism = \\-isMagmaHomomorphism ; injective = injective } //-isMagmaMonomorphism : //.IsMagmaMonomorphism ⟦_⟧ //-isMagmaMonomorphism = record { isMagmaHomomorphism = //-isMagmaHomomorphism ; injective = injective } open //.IsMagmaMonomorphism //-isMagmaMonomorphism public using (isRelMonomorphism) record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isQuasigroupMonomorphism : IsQuasigroupMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsQuasigroupMonomorphism isQuasigroupMonomorphism public ∙-isMagmaIsomorphism : ∙.IsMagmaIsomorphism ⟦_⟧ ∙-isMagmaIsomorphism = record { isMagmaMonomorphism = ∙-isMagmaMonomorphism ; surjective = surjective } \\-isMagmaIsomorphism : \\.IsMagmaIsomorphism ⟦_⟧ \\-isMagmaIsomorphism = record { isMagmaMonomorphism = \\-isMagmaMonomorphism ; surjective = surjective } //-isMagmaIsomorphism : //.IsMagmaIsomorphism ⟦_⟧ //-isMagmaIsomorphism = record { isMagmaMonomorphism = //-isMagmaMonomorphism ; surjective = surjective } open //.IsMagmaIsomorphism //-isMagmaIsomorphism public using (isRelIsomorphism) ------------------------------------------------------------------------ -- Morphisms over loop-like structures ------------------------------------------------------------------------ module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where open RawLoop L₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁; \\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁; _≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_; ε to ε₁) open RawLoop L₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂; \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂; _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_ ; ε to ε₂) open MorphismDefinitions A B _≈₂_ open FunctionDefinitions _≈₁_ _≈₂_ open QuasigroupMorphisms (RawLoop.rawQuasigroup L₁) (RawLoop.rawQuasigroup L₂) record IsLoopHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧ ε-homo : Homomorphic₀ ⟦_⟧ ε₁ ε₂ open IsQuasigroupHomomorphism isQuasigroupHomomorphism public record IsLoopMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isLoopHomomorphism : IsLoopHomomorphism ⟦_⟧ injective : Injective ⟦_⟧ open IsLoopHomomorphism isLoopHomomorphism public record IsLoopIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field isLoopMonomorphism : IsLoopMonomorphism ⟦_⟧ surjective : Surjective ⟦_⟧ open IsLoopMonomorphism isLoopMonomorphism public ------------------------------------------------------------------------ -- Re-export contents of modules publicly open MagmaMorphisms public open MonoidMorphisms public open GroupMorphisms public open NearSemiringMorphisms public open SemiringMorphisms public open RingMorphisms public open QuasigroupMorphisms public open LoopMorphisms public