fact: Definition iso_to_natTrans_inv {F G : functor C D } (phi : natIso F G) : natTrans G F := iso_to_natTrans (natIso_sym phi).
imports: Coq(ssreflect ssrfun) Coq.Relations(Relation_Definitions) Coq.Classes(RelationClasses Morphisms) Mon(SPropBase)