Lemma isalghom_pr1foldr : is_algebra_mor listFunctor List_alg List_alg (λ l, pr1 (foldr P'HSET P0' Pc' l)). Proof. apply (BinCoproductArrow_eq_cor _ BinCoproductsHSET). - apply funextfun; intro x; induction x. apply (maponpaths pr1 (foldr_nil P'HSET P0' Pc')). - apply funextfun; intro x; destruct x as [a l]. apply (maponpaths pr1 (foldr_cons P'HSET P0' Pc' a l)). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.PartA. 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.PrecategoryBinProduct.