------------------------------------------------------------------------
-- 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