{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} →
      {X : C} →
        {P : Sort u} →
          {toMonObj : CategoryTheory.MonObj X} →
            {inv : X ⟶ X} →
              {left_inv :
                  autoParam
                    (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X))
                        CategoryTheory.MonObj.mul =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                        CategoryTheory.MonObj.one)
                    CategoryTheory.GrpObj.left_inv._autoParam} →
                {right_inv :
                    autoParam
                      (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv)
                          CategoryTheory.MonObj.mul =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                          CategoryTheory.MonObj.one)
                      CategoryTheory.GrpObj.right_inv._autoParam} →
                  {toMonObj' : CategoryTheory.MonObj X} →
                    {inv' : X ⟶ X} →
                      {left_inv' :
                          autoParam
                            (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.CartesianMonoidalCategory.lift inv'
                                  (CategoryTheory.CategoryStruct.id X))
                                CategoryTheory.MonObj.mul =
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
                                CategoryTheory.MonObj.one)
                            CategoryTheory.GrpObj.left_inv._autoParam} →
                        {right_inv' :
                            autoParam
                              (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X)
                                    inv')
                                  CategoryTheory.MonObj.mul =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one)
                              CategoryTheory.GrpObj.right_inv._autoParam} →
                          { toMonObj := toMonObj, inv := inv, left_inv := left_inv, right_inv := right_inv } =
                              { toMonObj := toMonObj', inv := inv', left_inv := left_inv', right_inv := right_inv' } →
                            (toMonObj ≍ toMonObj' → inv ≍ inv' → P) → P