fact: Record LaxMorphLeftAdj := mkLaxMorphLeftAdj { lmlad_KD : lord_functor D1 D2 ; lmlad_KC : ord_functor C1 C2 ; lmlad_baseIso : natIso J2 (ord_functor_comp J1 lmlad_KC) ; lmlad_alpha : lnatTrans (lord_functor_comp (strict2laxFunc L1) lmlad_KD) (lord_functor_comp (strict2laxFunc (ord_functor_id _)) (strict2laxFunc L2)) ; lmlad_beta : lnatTrans (lord_functor_comp (strict2laxFunc R1) (strict2laxFunc lmlad_KC)) (lord_functor_comp lmlad_KD (strict2laxFunc R2)) ; lmlad_laxRetPres : forall {A}, (paste lmlad_alpha lmlad_beta) A ∙ (lofmap (strict2laxFunc lmlad_KC) (η M1 A)) ∙ lmlad_baseIso A ⪷ (η M2 A) ; lmlad_StrucIsoPres : forall A Y (f : D1⦅L1 A ; Y⦆), lofmap lmlad_KD f = ((natIso_sym phi2)⟨A,lmlad_KD Y⟩)∙1 (lmlad_beta Y ∙ ofmap lmlad_KC ( (phi1 ⟨A,Y⟩) ∙1 f ) ∙ lmlad_baseIso A) ∙ lmlad_alpha A }.
imports: Relational(OrderEnrichedCategory) Mon(SPropBase) mathcomp(all_ssreflect boolp) Crypt(Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf)