{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {motive : CategoryTheory.PreGaloisCategory C → Sort u} →
      ((hasTerminal : CategoryTheory.Limits.HasTerminal C) →
          (hasPullbacks : CategoryTheory.Limits.HasPullbacks C) →
            (hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C) →
              (hasQuotientsByFiniteGroups :
                  ∀ (G : Type u₂) [inst_1 : Group G] [Finite G],
                    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C) →
                (monoInducesIsoOnDirectSummand :
                    ∀ {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i],
                      ∃ Z u, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))) →
                  motive ⋯) →
        (t : CategoryTheory.PreGaloisCategory C) → motive t