proposition: Lemma gcm_joinE : Join X = necset_join X.
proof: Proof. apply/necset_ext. rewrite /= /join_ /= /Monad_of_category_monad.join /= !HCompId !HIdComp eps1E. rewrite functor_o NEqE functor_id compfid. rewrite 2!VCompE_nat HCompId HIdComp. set E := epsC _; have->: E = [hom idfun] by apply/hom_ext; rewrite epsCE. rewrite functor_id_hom. rewrite !functor_o functor_id !compfid. set F1J := F1 # _. have-> : F1J = @necset_join.F1join0 _ :> (_ -> _). - apply funext=> x; apply necset_ext=> /=. rewrite /F1J /= /necset_join.F1join0' /=. cbn. rewrite /free_semiCompSemiLattConvType_mor; unlock=> /=. by rewrite eps0E. congr hull; apply: classical_sets.eq_bigcup; first by rewrite -eqEsubset. by move=> x nXx; case: ifPn => // /negP; rewrite in_setE. 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 hierarchy