Set-magmoids

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-01.
Last modified on 2024-02-06.

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 in one sense the "oidification" of magmas in sets. We call elements of the indexing type objects, and elements of the set-family morphisms or homomorphisms.

These objects serve as our starting point in the study of the stucture 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-set x x are both right and left units with regard to composition. It is enough to show that e ＝ e' since the right and left unit laws are propositions (because all hom-types are sets). By function extensionality, it is enough to show that e x ＝ e' x for all x : A. But by the unit laws we have the following chain of equalities: 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