Set-magmoids

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-01.

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