Lemma foldr_node (X : hSet) (x : X) (f : pr1 A × X × X -> X) (a : pr1 A) (l1 l2 : pr1 Tree) : foldr X x f (node (a,,l1,,l2)) = f (a,,foldr X x f l1,,foldr X x f l2). Proof. assert (F := maponpaths (λ x, BinCoproductIn2 (BinCoproductsHSET _ _)· x) (algebra_mor_commutes _ _ _ (foldr_map X x f))). assert (Fal := toforallpaths _ _ _ F (a,,l1,,l2)). clear F. unfold compose in Fal. simpl in Fal. apply Fal. Opaque foldr_map. Qed.
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.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.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Inductives.Lists.