proposition: Corollary Opposite_Transform_invol `{F : C ⟶ D} {G : C ⟶ D} `(N : F ⟹ G) : (N^op)^op = N.
proof: Proof. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Natural.Transformation Category.Construction.Opposite Category.Functor.Opposite