Products of magmas

Content created by Garrett Figueroa.

Created on 2025-08-03.
Last modified on 2025-08-03.

module structured-types.product-magmas where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.magmas

Idea

For any pair of magmas M and N, their cartesian product M × N carries a natural magma structure.

Definition

module _
  {l1 l2 : Level} (M : Magma l1) (N : Magma l2)
  where

  product-Magma : Magma (l1 ⊔ l2)
  pr1 product-Magma = type-Magma M × type-Magma N
  pr2 product-Magma (x , y) (z , w) = mul-Magma M x z , mul-Magma N y w

Recent changes