------------------------------------------------------------------------
-- The Agda standard library
--
-- Instances of algebraic structures made by taking two other instances
-- A and B, and having elements of the new instance be pairs |A| × |B|.
-- In mathematics, this would usually be written A × B or A ⊕ B.
--
-- From semigroups up, these new instances are products of the relevant
-- category. For structures with commutative addition (commutative
-- monoids, Abelian groups, semirings, rings), the direct product is
-- also the coproduct, making it a biproduct.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Construct.DirectProduct where
open import Algebra
open import Data.Product.Base using (_×_; zip; _,_; map; _<*>_; uncurry)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Level using (Level; _⊔_)
private
variable
a b ℓ₁ ℓ₂ : Level
------------------------------------------------------------------------
-- Raw bundles
rawMagma : RawMagma a ℓ₁ → RawMagma b ℓ₂ → RawMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawMagma M N = record
{ Carrier = M.Carrier × N.Carrier
; _≈_ = Pointwise M._≈_ N._≈_
; _∙_ = zip M._∙_ N._∙_
} where module M = RawMagma M; module N = RawMagma N
rawMonoid : RawMonoid a ℓ₁ → RawMonoid b ℓ₂ → RawMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawMonoid M N = record
{ Carrier = M.Carrier × N.Carrier
; _≈_ = Pointwise M._≈_ N._≈_
; _∙_ = zip M._∙_ N._∙_
; ε = M.ε , N.ε
} where module M = RawMonoid M; module N = RawMonoid N
rawGroup : RawGroup a ℓ₁ → RawGroup b ℓ₂ → RawGroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawGroup G H = record
{ Carrier = G.Carrier × H.Carrier
; _≈_ = Pointwise G._≈_ H._≈_
; _∙_ = zip G._∙_ H._∙_
; ε = G.ε , H.ε
; _⁻¹ = map G._⁻¹ H._⁻¹
} where module G = RawGroup G; module H = RawGroup H
rawSemiring : RawSemiring a ℓ₁ → RawSemiring b ℓ₂ → RawSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawSemiring R S = record
{ Carrier = R.Carrier × S.Carrier
; _≈_ = Pointwise R._≈_ S._≈_
; _+_ = zip R._+_ S._+_
; _*_ = zip R._*_ S._*_
; 0# = R.0# , S.0#
; 1# = R.1# , S.1#
} where module R = RawSemiring R; module S = RawSemiring S
rawRingWithoutOne : RawRingWithoutOne a ℓ₁ → RawRingWithoutOne b ℓ₂ → RawRingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawRingWithoutOne R S = record
{ Carrier = R.Carrier × S.Carrier
; _≈_ = Pointwise R._≈_ S._≈_
; _+_ = zip R._+_ S._+_
; _*_ = zip R._*_ S._*_
; -_ = map R.-_ S.-_
; 0# = R.0# , S.0#
} where module R = RawRingWithoutOne R; module S = RawRingWithoutOne S
rawRing : RawRing a ℓ₁ → RawRing b ℓ₂ → RawRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawRing R S = record
{ Carrier = R.Carrier × S.Carrier
; _≈_ = Pointwise R._≈_ S._≈_
; _+_ = zip R._+_ S._+_
; _*_ = zip R._*_ S._*_
; -_ = map R.-_ S.-_
; 0# = R.0# , S.0#
; 1# = R.1# , S.1#
} where module R = RawRing R; module S = RawRing S
rawQuasigroup : RawQuasigroup a ℓ₁ → RawQuasigroup b ℓ₂ → RawQuasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawQuasigroup M N = record
{ Carrier = M.Carrier × N.Carrier
; _≈_ = Pointwise M._≈_ N._≈_
; _∙_ = zip M._∙_ N._∙_
; _\\_ = zip M._\\_ N._\\_
; _//_ = zip M._//_ N._//_
} where module M = RawQuasigroup M; module N = RawQuasigroup N
rawLoop : RawLoop a ℓ₁ → RawLoop b ℓ₂ → RawLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rawLoop M N = record
{ Carrier = M.Carrier × N.Carrier
; _≈_ = Pointwise M._≈_ N._≈_
; _∙_ = zip M._∙_ N._∙_
; _\\_ = zip M._\\_ N._\\_
; _//_ = zip M._//_ N._//_
; ε = M.ε , N.ε
} where module M = RawLoop M; module N = RawLoop N
------------------------------------------------------------------------
-- Bundles
magma : Magma a ℓ₁ → Magma b ℓ₂ → Magma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
magma M N = record
{ Carrier = M.Carrier × N.Carrier
; _≈_ = Pointwise M._≈_ N._≈_
; _∙_ = zip M._∙_ N._∙_
; isMagma = record
{ isEquivalence = ×-isEquivalence M.isEquivalence N.isEquivalence
; ∙-cong = zip M.∙-cong N.∙-cong
}
} where module M = Magma M; module N = Magma N
idempotentMagma : IdempotentMagma a ℓ₁ → IdempotentMagma b ℓ₂ → IdempotentMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
idempotentMagma G H = record
{ isIdempotentMagma = record
{ isMagma = Magma.isMagma (magma G.magma H.magma)
; idem = λ x → (G.idem , H.idem) <*> x
}
} where module G = IdempotentMagma G; module H = IdempotentMagma H
alternativeMagma : AlternativeMagma a ℓ₁ → AlternativeMagma b ℓ₂ → AlternativeMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
alternativeMagma G H = record
{ isAlternativeMagma = record
{ isMagma = Magma.isMagma (magma G.magma H.magma)
; alter = (λ x y → G.alternativeˡ , H.alternativeˡ <*> x <*> y)
, (λ x y → G.alternativeʳ , H.alternativeʳ <*> x <*> y)
}
} where module G = AlternativeMagma G; module H = AlternativeMagma H
flexibleMagma : FlexibleMagma a ℓ₁ → FlexibleMagma b ℓ₂ → FlexibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
flexibleMagma G H = record
{ isFlexibleMagma = record
{ isMagma = Magma.isMagma (magma G.magma H.magma)
; flex = λ x y → (G.flex , H.flex) <*> x <*> y
}
} where module G = FlexibleMagma G; module H = FlexibleMagma H
medialMagma : MedialMagma a ℓ₁ → MedialMagma b ℓ₂ → MedialMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
medialMagma G H = record
{ isMedialMagma = record
{ isMagma = Magma.isMagma (magma G.magma H.magma)
; medial = λ x y u z → (G.medial , H.medial) <*> x <*> y <*> u <*> z
}
} where module G = MedialMagma G; module H = MedialMagma H
semimedialMagma : SemimedialMagma a ℓ₁ → SemimedialMagma b ℓ₂ → SemimedialMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
semimedialMagma G H = record
{ isSemimedialMagma = record
{ isMagma = Magma.isMagma (magma G.magma H.magma)
; semiMedial = (λ x y z → G.semimedialˡ , H.semimedialˡ <*> x <*> y <*> z)
, ((λ x y z → G.semimedialʳ , H.semimedialʳ <*> x <*> y <*> z))
}
} where module G = SemimedialMagma G; module H = SemimedialMagma H
semigroup : Semigroup a ℓ₁ → Semigroup b ℓ₂ → Semigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
semigroup G H = record
{ isSemigroup = record
{ isMagma = Magma.isMagma (magma G.magma H.magma)
; assoc = λ x y z → (G.assoc , H.assoc) <*> x <*> y <*> z
}
} where module G = Semigroup G; module H = Semigroup H
band : Band a ℓ₁ → Band b ℓ₂ → Band (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
band B C = record
{ isBand = record
{ isSemigroup = Semigroup.isSemigroup (semigroup B.semigroup C.semigroup)
; idem = λ x → (B.idem , C.idem) <*> x
}
} where module B = Band B; module C = Band C
commutativeSemigroup : CommutativeSemigroup a ℓ₁ → CommutativeSemigroup b ℓ₂ →
CommutativeSemigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
commutativeSemigroup G H = record
{ isCommutativeSemigroup = record
{ isSemigroup = Semigroup.isSemigroup (semigroup G.semigroup H.semigroup)
; comm = λ x y → (G.comm , H.comm) <*> x <*> y
}
} where module G = CommutativeSemigroup G; module H = CommutativeSemigroup H
unitalMagma : UnitalMagma a ℓ₁ → UnitalMagma b ℓ₂ → UnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
unitalMagma M N = record
{ ε = M.ε , N.ε
; isUnitalMagma = record
{ isMagma = Magma.isMagma (magma M.magma N.magma)
; identity = (M.identityˡ , N.identityˡ <*>_)
, (M.identityʳ , N.identityʳ <*>_)
}
} where module M = UnitalMagma M; module N = UnitalMagma N
monoid : Monoid a ℓ₁ → Monoid b ℓ₂ → Monoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
monoid M N = record
{ ε = M.ε , N.ε
; isMonoid = record
{ isSemigroup = Semigroup.isSemigroup (semigroup M.semigroup N.semigroup)
; identity = (M.identityˡ , N.identityˡ <*>_)
, (M.identityʳ , N.identityʳ <*>_)
}
} where module M = Monoid M; module N = Monoid N
commutativeMonoid : CommutativeMonoid a ℓ₁ → CommutativeMonoid b ℓ₂ →
CommutativeMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
commutativeMonoid M N = record
{ isCommutativeMonoid = record
{ isMonoid = Monoid.isMonoid (monoid M.monoid N.monoid)
; comm = λ x y → (M.comm , N.comm) <*> x <*> y
}
} where module M = CommutativeMonoid M; module N = CommutativeMonoid N
idempotentCommutativeMonoid :
IdempotentCommutativeMonoid a ℓ₁ → IdempotentCommutativeMonoid b ℓ₂ →
IdempotentCommutativeMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
idempotentCommutativeMonoid M N = record
{ isIdempotentCommutativeMonoid = record
{ isCommutativeMonoid = CommutativeMonoid.isCommutativeMonoid
(commutativeMonoid M.commutativeMonoid N.commutativeMonoid)
; idem = λ x → (M.idem , N.idem) <*> x
}
}
where
module M = IdempotentCommutativeMonoid M
module N = IdempotentCommutativeMonoid N
invertibleMagma : InvertibleMagma a ℓ₁ → InvertibleMagma b ℓ₂ → InvertibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
invertibleMagma M N = record
{ _⁻¹ = map M._⁻¹ N._⁻¹
; isInvertibleMagma = record
{ isMagma = Magma.isMagma (magma M.magma N.magma)
; inverse = (λ x → (M.inverseˡ , N.inverseˡ) <*> x)
, (λ x → (M.inverseʳ , N.inverseʳ) <*> x)
; ⁻¹-cong = map M.⁻¹-cong N.⁻¹-cong
}
} where module M = InvertibleMagma M; module N = InvertibleMagma N
invertibleUnitalMagma : InvertibleUnitalMagma a ℓ₁ → InvertibleUnitalMagma b ℓ₂ → InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
invertibleUnitalMagma M N = record
{ ε = M.ε , N.ε
; isInvertibleUnitalMagma = record
{ isInvertibleMagma = InvertibleMagma.isInvertibleMagma (invertibleMagma M.invertibleMagma N.invertibleMagma)
; identity = (M.identityˡ , N.identityˡ <*>_)
, (M.identityʳ , N.identityʳ <*>_)
}
} where module M = InvertibleUnitalMagma M; module N = InvertibleUnitalMagma N
group : Group a ℓ₁ → Group b ℓ₂ → Group (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
group G H = record
{ _⁻¹ = map G._⁻¹ H._⁻¹
; isGroup = record
{ isMonoid = Monoid.isMonoid (monoid G.monoid H.monoid)
; inverse = (λ x → (G.inverseˡ , H.inverseˡ) <*> x)
, (λ x → (G.inverseʳ , H.inverseʳ) <*> x)
; ⁻¹-cong = map G.⁻¹-cong H.⁻¹-cong
}
} where module G = Group G; module H = Group H
abelianGroup : AbelianGroup a ℓ₁ → AbelianGroup b ℓ₂ →
AbelianGroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
abelianGroup G H = record
{ isAbelianGroup = record
{ isGroup = Group.isGroup (group G.group H.group)
; comm = λ x y → (G.comm , H.comm) <*> x <*> y
}
} where module G = AbelianGroup G; module H = AbelianGroup H
semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ₁ →
SemiringWithoutAnnihilatingZero b ℓ₂ →
SemiringWithoutAnnihilatingZero (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
semiringWithoutAnnihilatingZero R S = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = CommutativeMonoid.isCommutativeMonoid
(commutativeMonoid R.+-commutativeMonoid
S.+-commutativeMonoid)
; *-cong = zip R.*-cong S.*-cong
; *-assoc = λ x y z → (R.*-assoc , S.*-assoc) <*> x <*> y <*> z
; *-identity = (R.*-identityˡ , S.*-identityˡ <*>_)
, (R.*-identityʳ , S.*-identityʳ <*>_)
; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
, (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
}
} where module R = SemiringWithoutAnnihilatingZero R
module S = SemiringWithoutAnnihilatingZero S
semiring : Semiring a ℓ₁ → Semiring b ℓ₂ → Semiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
semiring R S = record
{ isSemiring = record
{ isSemiringWithoutAnnihilatingZero =
SemiringWithoutAnnihilatingZero.isSemiringWithoutAnnihilatingZero U
; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)
, uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)
}
}
where
module R = Semiring R
module S = Semiring S
U = semiringWithoutAnnihilatingZero R.semiringWithoutAnnihilatingZero
S.semiringWithoutAnnihilatingZero
commutativeSemiring : CommutativeSemiring a ℓ₁ → CommutativeSemiring b ℓ₂ →
CommutativeSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
commutativeSemiring R S = record
{ isCommutativeSemiring = record
{ isSemiring = Semiring.isSemiring (semiring R.semiring S.semiring)
; *-comm = λ x y → (R.*-comm , S.*-comm) <*> x <*> y
}
} where module R = CommutativeSemiring R; module S = CommutativeSemiring S
idempotentSemiring : IdempotentSemiring a ℓ₁ → IdempotentSemiring b ℓ₂ → IdempotentSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
idempotentSemiring K L = record
{ isIdempotentSemiring = record
{ isSemiring = Semiring.isSemiring (semiring K.semiring L.semiring)
; +-idem = λ x → (K.+-idem , L.+-idem) <*> x
}
} where module K = IdempotentSemiring K; module L = IdempotentSemiring L
kleeneAlgebra : KleeneAlgebra a ℓ₁ → KleeneAlgebra b ℓ₂ → KleeneAlgebra (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
kleeneAlgebra K L = record
{ isKleeneAlgebra = record
{ isIdempotentSemiring = IdempotentSemiring.isIdempotentSemiring (idempotentSemiring K.idempotentSemiring L.idempotentSemiring)
; starExpansive = (λ x → (K.starExpansiveˡ , L.starExpansiveˡ) <*> x)
, (λ x → (K.starExpansiveʳ , L.starExpansiveʳ) <*> x)
; starDestructive = (λ a b x x₁ → (K.starDestructiveˡ , L.starDestructiveˡ) <*> a <*> b <*> x <*> x₁)
, (λ a b x x₁ → (K.starDestructiveʳ , L.starDestructiveʳ) <*> a <*> b <*> x <*> x₁)
}
} where module K = KleeneAlgebra K; module L = KleeneAlgebra L
ringWithoutOne : RingWithoutOne a ℓ₁ → RingWithoutOne b ℓ₂ → RingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
ringWithoutOne R S = record
{ isRingWithoutOne = record
{ +-isAbelianGroup = AbelianGroup.isAbelianGroup ((abelianGroup R.+-abelianGroup S.+-abelianGroup))
; *-cong = Semigroup.∙-cong (semigroup R.*-semigroup S.*-semigroup)
; *-assoc = Semigroup.assoc (semigroup R.*-semigroup S.*-semigroup)
; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
, (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
}
} where module R = RingWithoutOne R; module S = RingWithoutOne S
nonAssociativeRing : NonAssociativeRing a ℓ₁ → NonAssociativeRing b ℓ₂ → NonAssociativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
nonAssociativeRing R S = record
{ isNonAssociativeRing = record
{ +-isAbelianGroup = AbelianGroup.isAbelianGroup ((abelianGroup R.+-abelianGroup S.+-abelianGroup))
; *-cong = UnitalMagma.∙-cong (unitalMagma R.*-unitalMagma S.*-unitalMagma)
; *-identity = UnitalMagma.identity (unitalMagma R.*-unitalMagma S.*-unitalMagma)
; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
, (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)
, uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)
}
} where module R = NonAssociativeRing R; module S = NonAssociativeRing S
quasiring : Quasiring a ℓ₁ → Quasiring b ℓ₂ → Quasiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
quasiring R S = record
{ isQuasiring = record
{ +-isMonoid = Monoid.isMonoid ((monoid R.+-monoid S.+-monoid))
; *-cong = Monoid.∙-cong (monoid R.*-monoid S.*-monoid)
; *-assoc = Monoid.assoc (monoid R.*-monoid S.*-monoid)
; *-identity = Monoid.identity ((monoid R.*-monoid S.*-monoid))
; distrib = (λ x y z → (R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
, (λ x y z → (R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
; zero = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)
, uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)
}
} where module R = Quasiring R; module S = Quasiring S
nearring : Nearring a ℓ₁ → Nearring b ℓ₂ → Nearring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
nearring R S = record
{ isNearring = record
{ isQuasiring = Quasiring.isQuasiring (quasiring R.quasiring S.quasiring)
; +-inverse = (λ x → (R.+-inverseˡ , S.+-inverseˡ) <*> x)
, (λ x → (R.+-inverseʳ , S.+-inverseʳ) <*> x)
; ⁻¹-cong = map R.⁻¹-cong S.⁻¹-cong
}
} where module R = Nearring R; module S = Nearring S
ring : Ring a ℓ₁ → Ring b ℓ₂ → Ring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
ring R S = record
{ -_ = uncurry (λ x y → R.-_ x , S.-_ y)
; isRing = record
{ +-isAbelianGroup = AbelianGroup.isAbelianGroup A
; *-cong = Semiring.*-cong Semi
; *-assoc = Semiring.*-assoc Semi
; *-identity = Semiring.*-identity Semi
; distrib = Semiring.distrib Semi
}
}
where
module R = Ring R
module S = Ring S
Semi = semiring R.semiring S.semiring
A = abelianGroup R.+-abelianGroup S.+-abelianGroup
commutativeRing : CommutativeRing a ℓ₁ → CommutativeRing b ℓ₂ →
CommutativeRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
commutativeRing R S = record
{ isCommutativeRing = record
{ isRing = Ring.isRing (ring R.ring S.ring)
; *-comm = λ x y → (R.*-comm , S.*-comm) <*> x <*> y
}
} where module R = CommutativeRing R; module S = CommutativeRing S
quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
quasigroup M N = record
{ _\\_ = zip M._\\_ N._\\_
; _//_ = zip M._//_ N._//_
; isQuasigroup = record
{ isMagma = Magma.isMagma (magma M.magma N.magma)
; \\-cong = zip M.\\-cong N.\\-cong
; //-cong = zip M.//-cong N.//-cong
; leftDivides = (λ x y → M.leftDividesˡ , N.leftDividesˡ <*> x <*> y) , (λ x y → M.leftDividesʳ , N.leftDividesʳ <*> x <*> y)
; rightDivides = (λ x y → M.rightDividesˡ , N.rightDividesˡ <*> x <*> y) , (λ x y → M.rightDividesʳ , N.rightDividesʳ <*> x <*> y)
}
} where module M = Quasigroup M; module N = Quasigroup N
loop : Loop a ℓ₁ → Loop b ℓ₂ → Loop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
loop M N = record
{ ε = M.ε , N.ε
; isLoop = record
{ isQuasigroup = Quasigroup.isQuasigroup (quasigroup M.quasigroup N.quasigroup)
; identity = (M.identityˡ , N.identityˡ <*>_)
, (M.identityʳ , N.identityʳ <*>_)
}
} where module M = Loop M; module N = Loop N
leftBolLoop : LeftBolLoop a ℓ₁ → LeftBolLoop b ℓ₂ → LeftBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
leftBolLoop M N = record
{ isLeftBolLoop = record
{ isLoop = Loop.isLoop (loop M.loop N.loop)
; leftBol = λ x y z → M.leftBol , N.leftBol <*> x <*> y <*> z
}
} where module M = LeftBolLoop M; module N = LeftBolLoop N
rightBolLoop : RightBolLoop a ℓ₁ → RightBolLoop b ℓ₂ → RightBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
rightBolLoop M N = record
{ isRightBolLoop = record
{ isLoop = Loop.isLoop (loop M.loop N.loop)
; rightBol = λ x y z → M.rightBol , N.rightBol <*> x <*> y <*> z
}
} where module M = RightBolLoop M; module N = RightBolLoop N
middleBolLoop : MiddleBolLoop a ℓ₁ → MiddleBolLoop b ℓ₂ → MiddleBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
middleBolLoop M N = record
{ isMiddleBolLoop = record
{ isLoop = Loop.isLoop (loop M.loop N.loop)
; middleBol = λ x y z → M.middleBol , N.middleBol <*> x <*> y <*> z
}
} where module M = MiddleBolLoop M; module N = MiddleBolLoop N
moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
moufangLoop M N = record
{ isMoufangLoop = record
{ isLeftBolLoop = LeftBolLoop.isLeftBolLoop (leftBolLoop M.leftBolLoop N.leftBolLoop)
; rightBol = λ x y z → M.rightBol , N.rightBol <*> x <*> y <*> z
; identical = λ x y z → M.identical , N.identical <*> x <*> y <*> z
}
} where module M = MoufangLoop M; module N = MoufangLoop N
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