# Concrete monoids

Content created by Fredrik Bakke.

Created on 2023-09-15.

module group-theory.concrete-monoids where

Imports
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


## Idea

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.

## Definition

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)
where

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


## Properties

### 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)
where

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.