fact: Definition Opposite_Transform `{F : C ⟶ D} {G : C ⟶ D} `(N : F ⟹ G) : G^op ⟹ F^op := @Build_Transform (C^op) (D^op) (G^op) (F^op) N (λ (x y : (C ^op)%category) (f : x ~{C^op}~> y), @naturality_sym C D F G N y x f) (λ (x y : (C ^op)%category) (f : x ~{C^op}~> y), @naturality C D F G N y x f).
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Natural.Transformation Category.Construction.Opposite Category.Functor.Opposite