Lemma initialAlg_is_iso_subproof : is_inverse_in_precat a a'. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.Coproducts.