proposition: Lemma is_algebra_morphism_pr1_PL_fold : is_algebra_mor _ PL_alg PL_alg (λ l, pr1 (@PL_fold P'HSET P'_vars P'_not P'_and P'_or P'_impl l)).
proof: Proof. apply (BinCoproductArrow_eq_cor _ BinCoproductsHSET). - apply funextfun; intro x; induction x as [x2 | x3]. + induction x2 as [x4 | x5]. * induction x4 as [x6 | x7]. -- cbn in x6. Abort. End PL_ind. End PL. Definition bool_valuation {vars : hSet} (V : vars -> bool) : PL vars -> bool. Proof. use (@PL_fold vars boolset). - assumption. - exact negb. - exact andb. - exact orb. - exact implb. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Bool UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Chains.OmegaCocontFunctors UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Adamek