自己関手の代数

open import category-theory.category
open import category-theory.functor

module category-theory.algebra-for-functor
  {o h} {𝒞 : Category o h} (F : Functor 𝒞 𝒞) where

open import foundations.universe
open import foundations.identity-type
open import foundations.groupoid-laws
open import foundations.functions-are-functors
open import foundations.identity-type-reasoning
open Category 𝒞
private module F = Functor F

Algebra : Ob → Type h
Algebra A = Hom (F.₀ A) A

AlgebraHom : ∀ {A B} → Hom A B → Algebra A → Algebra B → Type h
AlgebraHom f α β = f ∘ α ＝ β ∘ F.₁ f

idAlgebraHom : ∀ {A} α → AlgebraHom (id A) α α
idAlgebraHom α =
  identˡ α ∙ sym (ap (α ∘_) (F.preserve-id _) ∙ identʳ α)

compAlgebraHom : ∀ {A B C} {g : Hom B C} {f : Hom A B}
  → ∀ {α β γ}
  → AlgebraHom g β γ → AlgebraHom f α β → AlgebraHom (g ∘ f) α γ
compAlgebraHom {g = g} {f = f} {α = α} {β} {γ} q p =
    (g ∘ f) ∘ α
  ＝⟨ assoc ⟩
    g ∘ (f ∘ α)
  ＝⟨ ap (g ∘_) p ⟩
    g ∘ (β ∘ F.₁ f)
  ＝⟨ sym assoc ⟩
    (g ∘ β) ∘ F.₁ f
  ＝⟨ ap (_∘ F.₁ f) q ⟩
    (γ ∘ F.₁ g) ∘ F.₁ f
  ＝⟨ assoc ⟩
    γ ∘ (F.₁ g ∘ F.₁ f)
  ＝⟨ ap (γ ∘_) (sym (F.preserve-∘ _ _)) ⟩
    γ ∘ F.₁ (g ∘ f)
  ∎