Sort u_1 →
  {C₀ : Type u₀} →
    {C : Type u} →
      [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
        [inst_1 : CategoryTheory.Category.{v, u} C] →
          {F : CategoryTheory.Functor C₀ C} →
            {S : C} →
              F.PreOneHypercoverDenseData S →
                {C₀' : Type u₀} →
                  {C' : Type u} →
                    [inst' : CategoryTheory.Category.{v₀, u₀} C₀'] →
                      [inst'_1 : CategoryTheory.Category.{v, u} C'] →
                        {F' : CategoryTheory.Functor C₀' C'} → {S' : C'} → F'.PreOneHypercoverDenseData S' → Sort u_1