{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} → {G : CategoryTheory.PreOneHypercover S} → E.Hom F → F.Hom G → E.Hom G