proposition: Lemma free_semiCompSemiLattConvType_mor_comp : FunctorLaws.comp free_semiCompSemiLattConvType_mor.
proof: Proof. move=> a b c [] g affine_g [] h affine_h; rewrite hom_ext funeqE => /= x /=. apply necset_ext => /=. rewrite 2!free_semiCompSemiLattConvType_morE' /= -image_comp. by rewrite free_semiCompSemiLattConvType_morE'. Qed.
imports: Reals mathcomp(all_ssreflect) mathcomp(boolp classical_sets) mathcomp(finmap) infotheo(Reals_ext classical_sets_ext ssrR ssr_ext) infotheo(fdist fsdist convex necset) monae_lib HB(structures) category