Commit 2026-03-13 18:43 bf9541ad

chore(CategoryTheory/Functor/Category): use to_dual (#36576) This PR uses to_dual on some theorems about the category instance of functor. to_dual can deal with Functor.category correctly, because the fields NatTrans and vcomp are already tagged to_dual and the arguments are swapped in the expected way. hcomp has two possible definitions that are dual to eachother and equivalent. For to_dual to use it, we need to prove that they are equivalent, with to_dual_insert_cast.