proposition: Lemma dsym_coupling { A B : ord_choiceType } { S1 S2 : choiceType } { d : SDistr_carrier (F_choice_prod_obj ⟨ Choice.Pack {| Choice.base := prod_eqMixin B S2; Choice.mixin := prod_choiceMixin B S2 |}, Choice.Pack {| Choice.base := prod_eqMixin A S1; Choice.mixin := prod_choiceMixin A S1 |} ⟩) } {d1 d2 } (Hcoupling : coupling d d1 d2) : coupling (dsym d) d2 d1.
proof: Proof. rewrite /dsym. destruct Hcoupling as [dfst_d dsnd_d]. unfold coupling, lmg, rmg in *. subst. split. - apply: distr_ext. exact: dfst_dswap d. - apply: distr_ext. exact: dsnd_dswap d. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum finmap.set finmap.finmap xfinmap) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type)