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
See also
- Nonunital precategories are associative set-magmoids.
- Precategories are associative and unital set-magmoids.
- Categories are univalent, associative and unital set-magmoids.
- Strict categories are associative and unital set-magmoids whose objects form a set.
External links
- magmoid at Lab
A wikidata identifier was not available for this concept.
Recent changes
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-09. Fredrik Bakke. Typeset
nlab
as$n$Lab
(#911). - 2023-11-01. Fredrik Bakke. Fun with functors (#886).