fact: Definition commuting_unary_base_square : natIso (choice_incl) (ord_functor_comp choice_incl (ord_functor_id TypeCat)).
imports: Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(ChoiceAsOrd Axioms RelativeMonadMorph_prod FreeProbProg SubDistr choice_type)