proposition: Lemma strucIso_rightAdj : (Phi ⟨A , B⟩)∙1 f = ofmap R f ∙ (η myM A).
proof: Proof. unshelve epose (Phi_nat := (ni_natural _ _ Phi)). exact ⟨A, L A⟩. exact ⟨A , B⟩. specialize (Phi_nat ⟨Id _, f⟩). simpl in Phi_nat. apply (f_equal sval) in Phi_nat. simpl in Phi_nat. unshelve eapply equal_f in Phi_nat. exact (Id _). cbv in Phi_nat. move: Phi_nat. rewrite !ord_cat_law2. rewrite !ord_functor_law1. rewrite !ord_cat_law2. move=> Phi_nat. assumption. Qed.
imports: Coq(Relation_Definitions Morphisms) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Mon(SPropBase) mathcomp(all_ssreflect boolp)