∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
  (η : X ⟶ Y),
  (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).left =
    (CategoryTheory.SimplicialObject.Augmented.drop.map η).app (Opposite.op (SimplexCategory.mk 0))