Set-magmoids

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-01.
Last modified on 2025-07-24.

module category-theory.set-magmoids where
Imports 
open import category-theory.composition-operations-on-binary-families-of-sets

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.sets
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.universe-levels

Idea

A set-magmoid is the structure of a composition operation on a binary family of sets, and are the oidification of magmas in sets in one sense of the term. We call elements of the indexing type objects, and elements of the set-family morphisms or homomorphisms.

Set-magmoids serve as our starting point in the study of the structure of categories. Indeed, categories form a subtype of set-magmoids, although structure-preserving maps of set-magmoids do not automatically preserve identity morphisms.

Set-magmoids are commonly referred to as magmoids in the literature, but we use the “set-” prefix to make clear its relation to magmas. Set-magmoids should not be confused with strict magmoids, which would be set-magmoids whose objects form a set.

Definitions

The type of set-magmoids

Set-Magmoid :
  (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Set-Magmoid l1 l2 =
  Σ ( UU l1)
    ( λ A →
      Σ ( A → A → Set l2)
        ( composition-operation-binary-family-Set))

module _
  {l1 l2 : Level} (M : Set-Magmoid l1 l2)
  where

  obj-Set-Magmoid : UU l1
  obj-Set-Magmoid = pr1 M

  hom-set-Set-Magmoid : (x y : obj-Set-Magmoid) → Set l2
  hom-set-Set-Magmoid = pr1 (pr2 M)

  hom-Set-Magmoid : (x y : obj-Set-Magmoid) → UU l2
  hom-Set-Magmoid x y = type-Set (hom-set-Set-Magmoid x y)

  is-set-hom-Set-Magmoid :
    (x y : obj-Set-Magmoid) → is-set (hom-Set-Magmoid x y)
  is-set-hom-Set-Magmoid x y =
    is-set-type-Set (hom-set-Set-Magmoid x y)

  comp-hom-Set-Magmoid :
    {x y z : obj-Set-Magmoid} →
    hom-Set-Magmoid y z →
    hom-Set-Magmoid x y →
    hom-Set-Magmoid x z
  comp-hom-Set-Magmoid = pr2 (pr2 M)

  comp-hom-Set-Magmoid' :
    {x y z : obj-Set-Magmoid} →
    hom-Set-Magmoid x y →
    hom-Set-Magmoid y z →
    hom-Set-Magmoid x z
  comp-hom-Set-Magmoid' f g = comp-hom-Set-Magmoid g f

The total hom-type of a set-magmoid

total-hom-Set-Magmoid :
  {l1 l2 : Level} (M : Set-Magmoid l1 l2) → UU (l1 ⊔ l2)
total-hom-Set-Magmoid M =
  Σ ( obj-Set-Magmoid M)
    ( λ x → Σ (obj-Set-Magmoid M) (hom-Set-Magmoid M x))

obj-total-hom-Set-Magmoid :
  {l1 l2 : Level} (M : Set-Magmoid l1 l2) →
  total-hom-Set-Magmoid M → obj-Set-Magmoid M × obj-Set-Magmoid M
pr1 (obj-total-hom-Set-Magmoid M (x , y , f)) = x
pr2 (obj-total-hom-Set-Magmoid M (x , y , f)) = y

Pre- and postcomposition by a morphism

module _
  {l1 l2 : Level} (M : Set-Magmoid l1 l2)
  {x y : obj-Set-Magmoid M}
  (f : hom-Set-Magmoid M x y)
  (z : obj-Set-Magmoid M)
  where

  precomp-hom-Set-Magmoid : hom-Set-Magmoid M y z → hom-Set-Magmoid M x z
  precomp-hom-Set-Magmoid g = comp-hom-Set-Magmoid M g f

  postcomp-hom-Set-Magmoid : hom-Set-Magmoid M z x → hom-Set-Magmoid M z y
  postcomp-hom-Set-Magmoid = comp-hom-Set-Magmoid M f

The predicate on set-magmoids of being associative

module _
  {l1 l2 : Level} (M : Set-Magmoid l1 l2)
  where

  is-associative-Set-Magmoid : UU (l1 ⊔ l2)
  is-associative-Set-Magmoid =
    is-associative-composition-operation-binary-family-Set
      ( hom-set-Set-Magmoid M)
      ( comp-hom-Set-Magmoid M)

  is-prop-is-associative-Set-Magmoid :
    is-prop
      ( is-associative-composition-operation-binary-family-Set
        ( hom-set-Set-Magmoid M)
        ( comp-hom-Set-Magmoid M))
  is-prop-is-associative-Set-Magmoid =
    is-prop-is-associative-composition-operation-binary-family-Set
      ( hom-set-Set-Magmoid M)
      ( comp-hom-Set-Magmoid M)

  is-associative-prop-Set-Magmoid : Prop (l1 ⊔ l2)
  is-associative-prop-Set-Magmoid =
    is-associative-prop-composition-operation-binary-family-Set
      ( hom-set-Set-Magmoid M)
      ( comp-hom-Set-Magmoid M)

The predicate on set-magmoids of being unital

Proof: To show that unitality is a proposition, suppose e e' : (x : A) → hom x x are both two-sided units with respect to composition. It is enough to show that e ＝ e' since the right and left unit laws are propositions by the set-condition on hom-types. By function extensionality, it is enough to show that e x ＝ e' x for all x : A, and by the unit laws we have:

  e x ＝ (e' x) ∘ (e x) ＝ e' x. ∎

module _
  {l1 l2 : Level} (M : Set-Magmoid l1 l2)
  where

  is-unital-Set-Magmoid : UU (l1 ⊔ l2)
  is-unital-Set-Magmoid =
    is-unital-composition-operation-binary-family-Set
      ( hom-set-Set-Magmoid M)
      ( comp-hom-Set-Magmoid M)

  is-prop-is-unital-Set-Magmoid :
    is-prop
      ( is-unital-composition-operation-binary-family-Set
        ( hom-set-Set-Magmoid M)
        ( comp-hom-Set-Magmoid M))
  is-prop-is-unital-Set-Magmoid =
    is-prop-is-unital-composition-operation-binary-family-Set
      ( hom-set-Set-Magmoid M)
      ( comp-hom-Set-Magmoid M)

  is-unital-prop-Set-Magmoid : Prop (l1 ⊔ l2)
  is-unital-prop-Set-Magmoid =
    is-unital-prop-composition-operation-binary-family-Set
      ( hom-set-Set-Magmoid M)
      ( comp-hom-Set-Magmoid M)

Properties

If the objects of a set-magmoid are k-truncated for nonnegative k, the total hom-type is k-truncated

module _
  {l1 l2 : Level} {k : 𝕋} (M : Set-Magmoid l1 l2)
  where

  is-trunc-total-hom-is-trunc-obj-Set-Magmoid :
    is-trunc (succ-𝕋 (succ-𝕋 k)) (obj-Set-Magmoid M) →
    is-trunc (succ-𝕋 (succ-𝕋 k)) (total-hom-Set-Magmoid M)
  is-trunc-total-hom-is-trunc-obj-Set-Magmoid is-trunc-obj-M =
    is-trunc-Σ
      ( is-trunc-obj-M)
      ( λ x →
        is-trunc-Σ
          ( is-trunc-obj-M)
          ( λ y → is-trunc-is-set k (is-set-hom-Set-Magmoid M x y)))

  total-hom-truncated-type-is-trunc-obj-Set-Magmoid :
    is-trunc (succ-𝕋 (succ-𝕋 k)) (obj-Set-Magmoid M) →
    Truncated-Type (l1 ⊔ l2) (succ-𝕋 (succ-𝕋 k))
  pr1 (total-hom-truncated-type-is-trunc-obj-Set-Magmoid is-trunc-obj-M) =
    total-hom-Set-Magmoid M
  pr2 (total-hom-truncated-type-is-trunc-obj-Set-Magmoid is-trunc-obj-M) =
    is-trunc-total-hom-is-trunc-obj-Set-Magmoid is-trunc-obj-M

See also

A wikidata identifier was not available for this concept.

Recent changes