Concrete monoids

Content created by Fredrik Bakke.

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

module group-theory.concrete-monoids where
open import category-theory.categories

open import foundation.0-connected-types
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import group-theory.cores-monoids
open import group-theory.monoids
open import group-theory.torsors


A concrete monoid, or univalent monoid, is the homotopy type theoretic analogue of monoids. We define it as a category whose type of objects is pointed and connected.


is-concrete-monoid-Category : {l1 l2 : Level}  Category l1 l2  UU l1
is-concrete-monoid-Category C = obj-Category C × is-0-connected (obj-Category C)

Concrete-Monoid : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Concrete-Monoid l1 l2 = Σ (Category l1 l2) (is-concrete-monoid-Category)

module _
  {l1 l2 : Level} (M : Concrete-Monoid l1 l2)

  category-Concrete-Monoid : Category l1 l2
  category-Concrete-Monoid = pr1 M

  is-concrete-monoid-category-Concrete-Monoid :
    is-concrete-monoid-Category category-Concrete-Monoid
  is-concrete-monoid-category-Concrete-Monoid = pr2 M


Concrete monoids from monoids

Given a monoid, we can define its associated concrete monoid. The type of objects is the classifying type of the core of the monoid. Moreover, we must take care in how we define the family of homomorphisms. They cannot simply be the constant family, as transporting along an invertible element should correspond to multiplying by the element in the family.

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

  obj-concrete-monoid-Monoid : UU (lsuc l)
  obj-concrete-monoid-Monoid = classifying-type-Group (core-Monoid M)

The remainder of the construction remains to be written down. We note that this is precisely the Rezk completion of the one object precategory associated to a monoid.

Recent changes