proposition: Lemma applied_ord_relmon_law2 : forall (A B : I) (f : TypeCat ⦅ J A; M B ⦆) x, dnib M f ( η M A x ) = f x.
proof: Proof. move=> A B f x. unshelve epose (aux := (ord_relmon_law2 M) _ _ _). shelve. shelve. exact f. unshelve eapply equal_f in aux. exact x. simpl in aux. assumption. Qed.
imports: Coq(Morphisms) mathcomp(all_ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd)