Morphisms of 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.morphisms-algebras-monads-on-precategories where
Imports
open import category-theory.algebras-monads-on-precategories open import category-theory.commuting-squares-of-morphisms-in-precategories open import category-theory.monads-on-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
Idea
A
morphism¶
between monad algebras
a : TA → A
and b : TB → B
is a map f : A → B
such that b ∘ Tf = f ∘ a
.
Definitions
module _ {l1 l2 : Level} (C : Precategory l1 l2) (T : monad-Precategory C) where coherence-morphism-algebra-monad-Precategory : (f g : algebra-monad-Precategory C T) → hom-Precategory C ( obj-algebra-monad-Precategory C T f) ( obj-algebra-monad-Precategory C T g) → UU l2 coherence-morphism-algebra-monad-Precategory f g h = coherence-square-hom-Precategory C ( hom-endofunctor-monad-Precategory C T h) ( hom-algebra-monad-Precategory C T f) ( hom-algebra-monad-Precategory C T g) ( h) morphism-algebra-monad-Precategory : (f g : algebra-monad-Precategory C T) → UU l2 morphism-algebra-monad-Precategory f g = Σ ( hom-Precategory C ( obj-algebra-monad-Precategory C T f) ( obj-algebra-monad-Precategory C T g)) ( coherence-morphism-algebra-monad-Precategory f g) hom-morphism-algebra-monad-Precategory : (f g : algebra-monad-Precategory C T) (h : morphism-algebra-monad-Precategory f g) → hom-Precategory C ( obj-algebra-monad-Precategory C T f) ( obj-algebra-monad-Precategory C T g) hom-morphism-algebra-monad-Precategory f g h = pr1 h top-hom-morphism-algebra-monad-Precategory : (f g : algebra-monad-Precategory C T) (h : morphism-algebra-monad-Precategory f g) → hom-Precategory C ( obj-endofunctor-monad-Precategory C T ( obj-algebra-monad-Precategory C T f)) ( obj-endofunctor-monad-Precategory C T ( obj-algebra-monad-Precategory C T g)) top-hom-morphism-algebra-monad-Precategory f g h = hom-endofunctor-monad-Precategory C T ( hom-morphism-algebra-monad-Precategory f g h) comm-hom-morphism-algebra-monad-Precategory : (f g : algebra-monad-Precategory C T) (h : morphism-algebra-monad-Precategory f g) → coherence-square-hom-Precategory C ( top-hom-morphism-algebra-monad-Precategory f g h) ( hom-algebra-monad-Precategory C T f) ( hom-algebra-monad-Precategory C T g) ( hom-morphism-algebra-monad-Precategory f g h) comm-hom-morphism-algebra-monad-Precategory f g h = pr2 h comp-morphism-algebra-monad-Precategory : (a b c : algebra-monad-Precategory C T) (g : morphism-algebra-monad-Precategory b c) → (f : morphism-algebra-monad-Precategory a b) → morphism-algebra-monad-Precategory a c comp-morphism-algebra-monad-Precategory a b c g f = ( comp-hom-Precategory C ( hom-morphism-algebra-monad-Precategory b c g) ( hom-morphism-algebra-monad-Precategory a b f)) , ( pasting-horizontal-coherence-square-hom-Precategory C ( top-hom-morphism-algebra-monad-Precategory a b f) ( top-hom-morphism-algebra-monad-Precategory b c g) ( hom-algebra-monad-Precategory C T a) ( hom-algebra-monad-Precategory C T b) ( hom-algebra-monad-Precategory C T c) ( hom-morphism-algebra-monad-Precategory a b f) ( hom-morphism-algebra-monad-Precategory b c g) ( comm-hom-morphism-algebra-monad-Precategory a b f) ( comm-hom-morphism-algebra-monad-Precategory b c g)) ∙ ( ap ( postcomp-hom-Precategory C (hom-algebra-monad-Precategory C T c) _) ( inv (preserves-comp-endofunctor-monad-Precategory C T _ _))) is-set-morphism-algebra-monad-Precategory : (f g : algebra-monad-Precategory C T) → is-set (morphism-algebra-monad-Precategory f g) is-set-morphism-algebra-monad-Precategory f g = is-set-Σ ( is-set-hom-Precategory C _ _) ( λ hk → is-set-is-prop (is-set-hom-Precategory C _ _ _ _))
Recent changes
- 2025-06-05. Ben Connors. Monad algebra fixes (#1441).
- 2025-06-04. Ben Connors and Fredrik Bakke. Work on monads and ordinary precategory adjunctions (#1427).