Definition preIt : D⟦L μF,X⟧ := colimArrow CC_LchnF X Pow_cocone. Local Lemma eqSS n : # L (e n) · preIt = Pow n IC z. Proof. apply (colimArrowCommutes CC_LchnF). Qed. Local Lemma is_z_iso_inF : is_z_isomorphism inF. Proof. apply initialAlg_is_z_iso, pr2. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Adamek. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.whiskering.