∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (φ : F ⟶ G)
  (x : F.Elements),
  (CategoryTheory.NatTrans.mapElements φ).obj x =
    match x with
    | ⟨X, x⟩ => ⟨X, φ.app X x⟩