One object precategories

Content created by Fredrik Bakke

Created on 2023-09-15.
Last modified on 2023-09-15.

module category-theory.one-object-precategories where
Imports 
open import category-theory.endomorphisms-in-precategories
open import category-theory.precategories

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.unit-type
open import foundation.universe-levels

open import group-theory.monoids

Definition

is-one-object-prop-Precategory : {l1 l2 : Level} → Precategory l1 l2 → Prop l1
is-one-object-prop-Precategory P = is-contr-Prop (obj-Precategory P)

is-one-object-Precategory : {l1 l2 : Level} → Precategory l1 l2 → UU l1
is-one-object-Precategory P = type-Prop (is-one-object-prop-Precategory P)

One-Object-Precategory : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
One-Object-Precategory l1 l2 = Σ (Precategory l1 l2) (is-one-object-Precategory)

module _
  {l1 l2 : Level} (P : One-Object-Precategory l1 l2)
  where

  precategory-One-Object-Precategory : Precategory l1 l2
  precategory-One-Object-Precategory = pr1 P

  is-one-object-precategory-One-Object-Precategory :
    is-one-object-Precategory precategory-One-Object-Precategory
  is-one-object-precategory-One-Object-Precategory = pr2 P

  object-One-Object-Precategory :
    obj-Precategory precategory-One-Object-Precategory
  object-One-Object-Precategory =
    center is-one-object-precategory-One-Object-Precategory

Properties

Monoids are one-object precategories

module _
  {l : Level} (M : Monoid l)
  where

  hom-one-object-precategory-Monoid :
    unit → unit → Set l
  hom-one-object-precategory-Monoid star star = set-Monoid M

  type-hom-one-object-precategory-Monoid :
    unit → unit → UU l
  type-hom-one-object-precategory-Monoid x y =
    type-Set (hom-one-object-precategory-Monoid x y)

  comp-hom-one-object-precategory-Monoid :
    {x y z : unit} →
    type-hom-one-object-precategory-Monoid y z →
    type-hom-one-object-precategory-Monoid x y →
    type-hom-one-object-precategory-Monoid x z
  comp-hom-one-object-precategory-Monoid {star} {star} {star} =
    mul-Monoid M

  associative-comp-hom-one-object-precategory-Monoid :
    {x y z w : unit} →
    (h : type-hom-one-object-precategory-Monoid z w)
    (g : type-hom-one-object-precategory-Monoid y z)
    (f : type-hom-one-object-precategory-Monoid x y) →
    comp-hom-one-object-precategory-Monoid
      ( comp-hom-one-object-precategory-Monoid h g)
      ( f) ＝
    comp-hom-one-object-precategory-Monoid
      ( h)
      ( comp-hom-one-object-precategory-Monoid g f)
  associative-comp-hom-one-object-precategory-Monoid
    {star} {star} {star} {star} =
    associative-mul-Monoid M

  associative-composition-structure-one-object-precategory-Monoid :
    associative-composition-structure-Set
      hom-one-object-precategory-Monoid
  pr1 associative-composition-structure-one-object-precategory-Monoid =
    comp-hom-one-object-precategory-Monoid
  pr2 associative-composition-structure-one-object-precategory-Monoid =
    associative-comp-hom-one-object-precategory-Monoid

  id-hom-one-object-precategory-Monoid :
    (x : unit) → type-hom-one-object-precategory-Monoid x x
  id-hom-one-object-precategory-Monoid star = unit-Monoid M

  left-unit-law-comp-hom-one-object-precategory-Monoid :
    {x y : unit} (f : type-hom-one-object-precategory-Monoid x y) →
    comp-hom-one-object-precategory-Monoid
      ( id-hom-one-object-precategory-Monoid y)
      ( f) ＝
    f
  left-unit-law-comp-hom-one-object-precategory-Monoid {star} {star} =
    left-unit-law-mul-Monoid M

  right-unit-law-comp-hom-one-object-precategory-Monoid :
    {x y : unit} (f : type-hom-one-object-precategory-Monoid x y) →
    comp-hom-one-object-precategory-Monoid
      ( f)
      ( id-hom-one-object-precategory-Monoid x) ＝
    f
  right-unit-law-comp-hom-one-object-precategory-Monoid {star} {star} =
    right-unit-law-mul-Monoid M

  is-unital-composition-structure-one-object-precategory-Monoid :
    is-unital-composition-structure-Set
      hom-one-object-precategory-Monoid
      associative-composition-structure-one-object-precategory-Monoid
  pr1 is-unital-composition-structure-one-object-precategory-Monoid =
    id-hom-one-object-precategory-Monoid
  pr1 (pr2 is-unital-composition-structure-one-object-precategory-Monoid) =
    left-unit-law-comp-hom-one-object-precategory-Monoid
  pr2 (pr2 is-unital-composition-structure-one-object-precategory-Monoid) =
    right-unit-law-comp-hom-one-object-precategory-Monoid

  precategory-one-object-precategory-Monoid : Precategory lzero l
  pr1 precategory-one-object-precategory-Monoid = unit
  pr1 (pr2 precategory-one-object-precategory-Monoid) =
    hom-one-object-precategory-Monoid
  pr1 (pr2 (pr2 precategory-one-object-precategory-Monoid)) =
    associative-composition-structure-one-object-precategory-Monoid
  pr2 (pr2 (pr2 precategory-one-object-precategory-Monoid)) =
    is-unital-composition-structure-one-object-precategory-Monoid

  one-object-precategory-Monoid : One-Object-Precategory lzero l
  pr1 one-object-precategory-Monoid = precategory-one-object-precategory-Monoid
  pr2 one-object-precategory-Monoid = is-contr-unit

Monoids from one-object precategories

monoid-One-Object-Precategory :
  {l1 l2 : Level} → One-Object-Precategory l1 l2 → Monoid l2
monoid-One-Object-Precategory P =
  monoid-endo-Precategory
    ( precategory-One-Object-Precategory P)
    ( object-One-Object-Precategory P)

Recent changes