∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ ⟶ F₂),
  (CategoryTheory.CategoryOfElements.map α).comp (CategoryTheory.CategoryOfElements.π F₂) =
    CategoryTheory.CategoryOfElements.π F₁