Unordered tuples of elements in commutative monoids

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-05-24.
Last modified on 2023-03-14.

module group-theory.unordered-tuples-of-elements-commutative-monoids where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels
open import foundation.unordered-tuples

open import group-theory.commutative-monoids

Definition

unordered-tuple-Commutative-Monoid :
  {l : Level} (n : ℕ) (M : Commutative-Monoid l) → UU (lsuc lzero ⊔ l)
unordered-tuple-Commutative-Monoid n M =
  unordered-tuple n (type-Commutative-Monoid M)

module _
  {l : Level} {n : ℕ} (M : Commutative-Monoid l)
  (x : unordered-tuple-Commutative-Monoid n M)
  where

  type-unordered-tuple-Commutative-Monoid : UU lzero
  type-unordered-tuple-Commutative-Monoid = type-unordered-tuple n x

  element-unordered-tuple-Commutative-Monoid :
    type-unordered-tuple-Commutative-Monoid → type-Commutative-Monoid M
  element-unordered-tuple-Commutative-Monoid =
    element-unordered-tuple n x

Recent changes