proposition: Lemma initialAlg_is_iso_subproof : is_inverse_in_precat a a'.
proof: Proof. assert (Ha'a : a' · a = identity A). { assert (algMor_a'a : is_algebra_mor _ _ _ (a' · a)). { unfold is_algebra_mor, a'; rewrite functor_comp. eapply pathscomp0; [|eapply cancel_postcomposition; apply Ha']. apply assoc. } apply pathsinv0; set (X := tpair _ _ algMor_a'a). apply (maponpaths pr1 (!@InitialEndo_is_identity _ AaInitial X)). } split; trivial. eapply pathscomp0; [apply Ha'|]; cbn. rewrite <- functor_comp. eapply pathscomp0; [eapply maponpaths; apply Ha'a|]. apply functor_id. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.NNO UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Limits.Coproducts