fact: Record OrderedMonadTransformer := mkOrderedMonadTransformer { mt_monad :> forall (M:OrderedMonad), OrderedMonadUnder M ; mt_map : forall (M1 M2:OrderedMonad), MonotonicMonadMorphism M1 M2 -> MonotonicMonadMorphism (mt_monad M1) (mt_monad M2) ; mt_map_id : forall M A m, mt_map (identity_monmon M) A m = identity_monmon _ A m ; mt_map_comp : forall (M1 M2 M3 : OrderedMonad) (θ12 : MonotonicMonadMorphism M1 M2) (θ23 : MonotonicMonadMorphism M2 M3) A m, mt_map θ23 _ (mt_map θ12 A m) = mt_map (comp_monmon θ12 θ23) A m ; mt_natural_lift : forall (M1 M2 : OrderedMonad) (θ : MonotonicMonadMorphism M1 M2) A m, mt_map θ _(mu_lift (mt_monad M1) A m) = mu_lift (mt_monad M2) _ (θ A m) }.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)