proposition: Lemma foldr_app (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧) (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) : app_map · foldr_map X fvar fapp flam = # (pr1 (Id * Id)) (foldr_map X fvar fapp flam) · fapp.
proof: Proof. assert (F := maponpaths (λ x, BinCoproductIn1 (BinCoproductsHSET2 _ _) · BinCoproductIn2 (BinCoproductsHSET2 _ _) · x) (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))). rewrite assoc in F. eapply pathscomp0; [apply F|]. rewrite assoc. eapply pathscomp0. eapply cancel_postcomposition. rewrite <- assoc. eapply maponpaths, BinCoproductOfArrowsIn2. rewrite assoc. eapply pathscomp0. eapply cancel_postcomposition, cancel_postcomposition, BinCoproductOfArrowsIn1. rewrite <- assoc. eapply pathscomp0; [eapply maponpaths, BinCoproductIn2Commutes|]. rewrite <- assoc. now eapply pathscomp0; [eapply maponpaths, BinCoproductIn1Commutes|]. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Adjunctions.Examples UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering