∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {X Y :
    CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C)
      (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))}
  (f : X ⟶ Y), CategoryTheory.CosimplicialObject.Augmented.drop.map f = f.right