fact: Definition hom_choiceType (a b : [the category of choiceType]) (f : a -> b) : {hom a, b} := Hom.Pack (Hom.Class (isHom.Axioms_ a b f I)).
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