F-algebra-category₀ : ∀ {i j} → (C : Category {i} {j}) → (F : Functor C C) →  Category₀ {j ⊔ i} {j ⊔ i}
F-algebra-category₀ {i} {j} C F =
 record {
  obj = F-algebra C F;
  hom = F-algebra-hom C F;
  id = λ Aα → record {
        f-hom = (Category.id C) (F-algebra.carrier Aα);
        hom-comm =
          ≡-⇶
           ((Category.left-id C) ((Functor.omap F) (F-algebra.carrier Aα)) (F-algebra.carrier Aα) (F-algebra.alg Aα))
           (≡-↑↓
              ([x≡y]→[Px→Py]
                  (λ x → ((Category.comp C) ((Functor.omap F) (F-algebra.carrier Aα)) ((Functor.omap F) (F-algebra.carrier Aα)) (F-algebra.carrier Aα) (F-algebra.alg Aα) x) ≡ (F-algebra.alg Aα))
                  ((Category.id C) ((Functor.omap F) (F-algebra.carrier Aα)))
                  ((Functor.fmap F) ((Category.id C) (F-algebra.carrier Aα)))
                  (≡-↑↓ ((Functor.preserves-id F) (F-algebra.carrier Aα)))
                  ((Category.right-id C) ((Functor.omap F) (F-algebra.carrier Aα)) (F-algebra.carrier Aα) (F-algebra.alg Aα))
              )
           )
       };

  comp = λ Aα Bβ Cγ g f → record {
           f-hom = (Category.comp C) (F-algebra.carrier Aα) (F-algebra.carrier Bβ) (F-algebra.carrier Cγ) (F-algebra-hom.f-hom g) (F-algebra-hom.f-hom f);
           hom-comm =  -- [g∘f]∘α ≡ γ∘[F[g]∘F[f]]
                    ≡-⇶ -- [g∘f]∘α ≡ g∘[f∘α]
                         (
                           (Category.assoc C)
                            ((Functor.omap F) (F-algebra.carrier Aα))
                            (F-algebra.carrier Aα)
                            (F-algebra.carrier Bβ)
                            (F-algebra.carrier Cγ)
                            (F-algebra-hom.f-hom g)
                            (F-algebra-hom.f-hom f)
                            (F-algebra.alg Aα)
                         )
                   (≡-⇶ -- g∘[f∘α] ≡ g∘[β∘F[f]]
                         (
                           [x≡y]→[fx≡fy]
                             ((Category.comp C)
                               ((Functor.omap F) (F-algebra.carrier Aα))
                               (F-algebra.carrier Bβ)
                               (F-algebra.carrier Cγ)
                               (F-algebra-hom.f-hom g)
                             )

                             ((Category.comp C)
                               ((Functor.omap F) (F-algebra.carrier Aα))
                               (F-algebra.carrier Aα)
                               (F-algebra.carrier Bβ)
                               (F-algebra-hom.f-hom f) (F-algebra.alg Aα)
                             )

                             ((Category.comp C)
                               ((Functor.omap F) (F-algebra.carrier Aα))
                               ((Functor.omap F) (F-algebra.carrier Bβ))
                               (F-algebra.carrier Bβ)
                               (F-algebra.alg Bβ)
                               ((Functor.fmap F) (F-algebra-hom.f-hom f))
                             )

                            (F-algebra-hom.hom-comm f)
                         )
                   (≡-⇶  -- g∘[β∘F[f]] ≡ [g∘β]∘F[f]
                          (≡-↑↓
                             (
                               (Category.assoc C)
                                   ((Functor.omap F) (F-algebra.carrier Aα))
                                   ((Functor.omap F) (F-algebra.carrier Bβ))
                                   (F-algebra.carrier Bβ)
                                   (F-algebra.carrier Cγ)
                                   (F-algebra-hom.f-hom g)
                                   (F-algebra.alg Bβ)
                                   ((Functor.fmap F) (F-algebra-hom.f-hom f))
                             )
                         )
                   (≡-⇶  -- [g∘β]∘F[f] ≡ [γ∘F[g]]∘F[f]
                           ([x≡y]→[fx≡fy]
                               (category-comp-rev C
                                  ((Functor.omap F) (F-algebra.carrier Aα))
                                  ((Functor.omap F) (F-algebra.carrier Bβ))
                                  (F-algebra.carrier Cγ)
                                  ((Functor.fmap F) (F-algebra-hom.f-hom f))
                               )

                               -- g∘β
                               ((Category.comp C)
                                  ((Functor.omap F) (F-algebra.carrier Bβ))
                                  (F-algebra.carrier Bβ)
                                  (F-algebra.carrier Cγ)
                                  (F-algebra-hom.f-hom g)
                                  (F-algebra.alg Bβ)
                               )
                               -- γ∘F[g]
                               ((Category.comp C)
                                  ((Functor.omap F) (F-algebra.carrier Bβ))
                                  ((Functor.omap F) (F-algebra.carrier Cγ))
                                  (F-algebra.carrier Cγ)
                                  (F-algebra.alg Cγ) ((Functor.fmap F) (F-algebra-hom.f-hom g))
                               )
                               -- g∘β≡γ∘F[g]
                               (F-algebra-hom.hom-comm g)
                         )

                   (≡-⇶ -- [γ∘F[g]]∘F[f] ≡ γ∘[F[g]∘F[f]]
                         (
                          (Category.assoc C)
                            ((Functor.omap F) (F-algebra.carrier Aα))
                            ((Functor.omap F) (F-algebra.carrier Bβ))
                            ((Functor.omap F) (F-algebra.carrier Cγ))
                            (F-algebra.carrier Cγ)
                            (F-algebra.alg Cγ)
                            ((Functor.fmap F) (F-algebra-hom.f-hom g))
                            ((Functor.fmap F) (F-algebra-hom.f-hom f))
                         )

                         -- γ∘[F[g]∘F[f]] ≡ γ∘[F[g∘f]]
                         (
                          [x≡y]→[fx≡fy]
                             ((Category.comp C)
                               ((Functor.omap F) (F-algebra.carrier Aα))
                               ((Functor.omap F) (F-algebra.carrier Cγ))
                               (F-algebra.carrier Cγ)
                               (F-algebra.alg Cγ)
                             )
                             ((Category.comp C)
                               ((Functor.omap F) (F-algebra.carrier Aα))
                               ((Functor.omap F) (F-algebra.carrier Bβ))
                               ((Functor.omap F) (F-algebra.carrier Cγ))
                               ((Functor.fmap F) (F-algebra-hom.f-hom g))
                               ((Functor.fmap F) (F-algebra-hom.f-hom f))
                             )
                             ((Functor.fmap F)
                                ((Category.comp C)
                                  (F-algebra.carrier Aα)
                                  (F-algebra.carrier Bβ)
                                  (F-algebra.carrier Cγ)
                                  (F-algebra-hom.f-hom g)
                                  (F-algebra-hom.f-hom f)
                                )
                             )
                             -- [F[g]∘F[f]] ≡ [F[g∘f]]
                             (≡-↑↓
                                ((Functor.preserves-comp F)
                                   (F-algebra.carrier Aα)
                                   (F-algebra.carrier Bβ)
                                   (F-algebra.carrier Cγ)
                                   (F-algebra-hom.f-hom f)
                                   (F-algebra-hom.f-hom g)
                                )
                             )
                         )

                   ))))
          }

 }