Algebras over monads on precategories

Content created by Ben Connors and Fredrik Bakke.

Created on 2025-06-04.
Last modified on 2025-06-05.

module category-theory.algebras-monads-on-precategories where
Imports 
open import category-theory.commuting-squares-of-morphisms-in-precategories
open import category-theory.functors-precategories
open import category-theory.monads-on-precategories
open import category-theory.natural-transformations-functors-precategories
open import category-theory.natural-transformations-maps-precategories
open import category-theory.precategories

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import foundation-core.cartesian-product-types

Idea

An algebra over a monad T consists of an object A and morphism a : TA → A satisfying two compatibility laws:

  • Unit law: a ∘ η_A = id_A
  • Multiplication law: a ∘ Ta = a ∘ μ_A

Definitions

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  (T : monad-Precategory C)
  where

  module _
    {A : obj-Precategory C}
    (a : hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A)
    where

    has-unit-law-algebra-monad-Precategory : UU l2
    has-unit-law-algebra-monad-Precategory =
      comp-hom-Precategory C a (hom-unit-monad-Precategory C T A) ＝
      id-hom-Precategory C

    has-mul-law-algebra-monad-Precategory : UU l2
    has-mul-law-algebra-monad-Precategory =
      comp-hom-Precategory C a (hom-endofunctor-monad-Precategory C T a) ＝
      comp-hom-Precategory C a (hom-mul-monad-Precategory C T A)

    is-algebra-monad-Precategory : UU l2
    is-algebra-monad-Precategory =
      has-unit-law-algebra-monad-Precategory ×
      has-mul-law-algebra-monad-Precategory

  algebra-monad-Precategory : UU (l1 ⊔ l2)
  algebra-monad-Precategory =
    Σ ( obj-Precategory C)
      ( λ A →
        Σ ( hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A)
          ( λ a → is-algebra-monad-Precategory a))

  obj-algebra-monad-Precategory : algebra-monad-Precategory → obj-Precategory C
  obj-algebra-monad-Precategory = pr1

  hom-algebra-monad-Precategory :
    (f : algebra-monad-Precategory) →
    hom-Precategory C
      ( obj-endofunctor-monad-Precategory C T (obj-algebra-monad-Precategory f))
      ( obj-algebra-monad-Precategory f)
  hom-algebra-monad-Precategory f = pr1 (pr2 f)

  comm-algebra-monad-Precategory :
    (f : algebra-monad-Precategory) →
    is-algebra-monad-Precategory (hom-algebra-monad-Precategory f)
  comm-algebra-monad-Precategory f = pr2 (pr2 f)

  unit-law-algebra-monad-Precategory :
    (f : algebra-monad-Precategory) →
    has-unit-law-algebra-monad-Precategory (hom-algebra-monad-Precategory f)
  unit-law-algebra-monad-Precategory f = pr1 (pr2 (pr2 f))

  mul-law-algebra-monad-Precategory :
    (f : algebra-monad-Precategory) →
    has-mul-law-algebra-monad-Precategory (hom-algebra-monad-Precategory f)
  mul-law-algebra-monad-Precategory f = pr2 (pr2 (pr2 f))

Recent changes