∀ (J : Type u₂) (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : J → C} (f : X ⟶ Y),
  (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as