proposition: Lemma FunpchoiceDr (A B : Type) (x y : gcm A) (k : A -> gcm B) p : (gcm # k) (x <|p|> y) = (gcm # k) x <|p|> (gcm # k) y.
proof: Proof. rewrite /hierarchy.actm /= /Monad_of_category_monad.actm /=. by rewrite scsl_hom_is_affine. Qed.
imports: Reals mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(boolp classical_sets) mathcomp(reals Rstruct) infotheo(classical_sets_ext Reals_ext ssrR fdist) infotheo(ssrR Reals_ext proba) infotheo(Reals_ext realType_ext) infotheo(fsdist convex necset) HB(structures) monae_lib hierarchy monad_lib proba_lib monad_model gcm_model category