Lemma foldr_lam (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧) (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) : lam_map · foldr_map X fvar fapp flam = # (pr1 (_ o option)) (foldr_map X fvar fapp flam) · flam. Proof. assert (F := maponpaths (λ x, BinCoproductIn2 (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, BinCoproductOfArrowsIn2. rewrite <- assoc. eapply pathscomp0. eapply maponpaths, BinCoproductIn2Commutes. rewrite <- assoc. now eapply pathscomp0; [eapply maponpaths, BinCoproductIn2Commutes|]. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Adjunctions.Examples. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering.