自己関手の代数の圏

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

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

open import foundations.universe
open import foundations.identity-type
open import foundations.greater-h-levels
open import category-theory.displayed-category
open import category-theory.algebra-for-functor F
open Category 𝒞 hiding (𝒞)
private module F = Functor F

Alg : DisplayedCategory 𝒞 h h
Alg = record
  { 𝒟 = record
    { Ob = Algebra
    ; Hom = AlgebraHom
    ; id = idAlgebraHom
    ; _∘_ = compAlgebraHom
    }
  ; is-displayed-category = record
    { identˡ = λ _ → is-set-hom _ _ _ _
    ; identʳ = λ _ → is-set-hom _ _ _ _
    ; ident² = λ _ → is-set-hom _ _ _ _
    ; assoc = is-set-hom _ _ _ _
    ; sym-assoc = is-set-hom _ _ _ _
    ; is-set-hom = isProp⇒isSet (is-set-hom _ _)
    }
  }