------------------------------------------------------------------------
-- The Agda standard library
--
-- The projection morphisms for algebraic structures arising from the
-- direct product construction
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Algebra.Morphism.Construct.DirectProduct where
open import Algebra.Bundles using (RawMagma; RawMonoid)
open import Algebra.Construct.DirectProduct using (rawMagma; rawMonoid)
open import Algebra.Morphism.Structures
using ( module MagmaMorphisms
; module MonoidMorphisms
)
open import Data.Product as Product
using (_,_)
open import Level using (Level)
open import Relation.Binary.Definitions using (Reflexive)
import Relation.Binary.Morphism.Construct.Product as RP
private
variable
a b c ℓ₁ ℓ₂ ℓ₃ : Level
------------------------------------------------------------------------
-- Magmas
module Magma (M : RawMagma a ℓ₁) (N : RawMagma b ℓ₂) where
open MagmaMorphisms
private
module M = RawMagma M
module N = RawMagma N
module Proj₁ (refl : Reflexive M._≈_) where
isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) M Product.proj₁
isMagmaHomomorphism = record
{ isRelHomomorphism = RP.proj₁
; homo = λ _ _ → refl
}
module Proj₂ (refl : Reflexive N._≈_) where
isMagmaHomomorphism : IsMagmaHomomorphism (rawMagma M N) N Product.proj₂
isMagmaHomomorphism = record
{ isRelHomomorphism = RP.proj₂
; homo = λ _ _ → refl
}
module Pair (P : RawMagma c ℓ₃) where
isMagmaHomomorphism : ∀ {f g} →
IsMagmaHomomorphism P M f →
IsMagmaHomomorphism P N g →
IsMagmaHomomorphism P (rawMagma M N) (Product.< f , g >)
isMagmaHomomorphism F G = record
{ isRelHomomorphism = RP.< F.isRelHomomorphism , G.isRelHomomorphism >
; homo = λ x y → F.homo x y , G.homo x y
}
where
module F = IsMagmaHomomorphism F
module G = IsMagmaHomomorphism G
-- Package for export
module Magma-Export {M : RawMagma a ℓ₁} {N : RawMagma b ℓ₂} where
open Magma
private
module M = RawMagma M
module N = RawMagma N
module _ {refl : Reflexive M._≈_} where
proj₁ = Proj₁.isMagmaHomomorphism M M refl
module _ {refl : Reflexive N._≈_} where
proj₂ = Proj₂.isMagmaHomomorphism M N refl
module _ {P : RawMagma c ℓ₃} where
<_,_> = Pair.isMagmaHomomorphism M N P
------------------------------------------------------------------------
-- Monoids
module Monoid (M : RawMonoid a ℓ₁) (N : RawMonoid b ℓ₂) where
open MonoidMorphisms
private
module M = RawMonoid M
module N = RawMonoid N
module Proj₁ (refl : Reflexive M._≈_) where
isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) M Product.proj₁
isMonoidHomomorphism = record
{ isMagmaHomomorphism = Magma.Proj₁.isMagmaHomomorphism M.rawMagma N.rawMagma refl
; ε-homo = refl
}
module Proj₂ (refl : Reflexive N._≈_) where
isMonoidHomomorphism : IsMonoidHomomorphism (rawMonoid M N) N Product.proj₂
isMonoidHomomorphism = record
{ isMagmaHomomorphism = Magma.Proj₂.isMagmaHomomorphism M.rawMagma N.rawMagma refl
; ε-homo = refl
}
module Pair (P : RawMonoid c ℓ₃) where
private
module P = RawMonoid P
isMonoidHomomorphism : ∀ {f g} →
IsMonoidHomomorphism P M f →
IsMonoidHomomorphism P N g →
IsMonoidHomomorphism P (rawMonoid M N) (Product.< f , g >)
isMonoidHomomorphism F G = record
{ isMagmaHomomorphism = Magma.Pair.isMagmaHomomorphism M.rawMagma N.rawMagma P.rawMagma F.isMagmaHomomorphism G.isMagmaHomomorphism
; ε-homo = F.ε-homo , G.ε-homo }
where
module F = IsMonoidHomomorphism F
module G = IsMonoidHomomorphism G
-- Package for export
module Monoid-Export {M : RawMonoid a ℓ₁} {N : RawMonoid b ℓ₂} where
open Monoid
private
module M = RawMonoid M
module N = RawMonoid N
module _ {refl : Reflexive M._≈_} where
proj₁ = Proj₁.isMonoidHomomorphism M M refl
module _ {refl : Reflexive N._≈_} where
proj₂ = Proj₂.isMonoidHomomorphism M N refl
module _ {P : RawMonoid c ℓ₃} where
<_,_> = Pair.isMonoidHomomorphism M N P
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