failure to recognize a `SSet` as a functor

Stream: mathlib4

[Emily Riehl]

There is an error in #25780 that I can't figure out. We're trying to apply Presheaf.colimitOfRepresentable to a simplicial set (a special case of a presheaf).

We think the problem may be some sort of universe error.

In a discussion over the infinity-cosmos channel @Thomas Murrills said:

Thomas Murrills said:

I'm also a little confused by lean's refusal to see X as something of type ?_ᵒᵖ ⥤ Type ?u after Presheaf.colimitOfRepresentable. If I try to recreate the issue with something like

def F {α} [Category α] (_ : αᵒᵖ ⥤ Type*) : True := trivial

variable (x : SSet.{u})

#check F x

it shows no signs of trouble.

If I add a coercion of the form

instance : Coe SSet.{u} (SimplexCategoryᵒᵖ ⥤ Type u) := ⟨id⟩

the application type mismatch for X disappears, and is replaced by a failure to synthesize a certain Category (which I believe, in this case, hints at the deeper universe issue I mentioned above).

I wonder if the application mismatch wouldn't have occurred if the typeclass synthesis would succeed, or something strange like that? (If so, I'd suspect that something to do with backtracking and/or metavariable synthesis order/postponement was to blame...)

@Bhavik Mehta or @Andrew Yang I think one of you may have written this code, which I'll admit I don't fully understand. In particular, what is CategoryTheory2?

[Thomas Murrills]

I'll also mention the universe issue itself here (which is buried in a bullet point in that thread, sorry):

Presheaf.colimitOfRepresentable makes a choice that constrains a universe in its argument to be smaller than necessary. (If it were too big, that would be fine—just ulift.) Generalizing this universe parameter in the original file seems plausible, but then the whole file needs to be reworked (starting all the way up at functorToRepresentables), uliftFunctors need to be inserted everywhere, potential pitfalls await, etc.

To be a bit more explicit, colimitOfRepresentable has type

def colimitOfRepresentable (P : Cᵒᵖ ⥤ Type v₁) : IsColimit (coconeOfRepresentable P)

but v₁ here is the universe level of the arrows of C. For SimplexCategory, that's 0 (or 1?), but SSet.{u} is SimplexCategoryᵒᵖ ⥤ Type u.

Ideally we would have (P : Cᵒᵖ ⥤ Type v₂), but starting on that journey in CategoryTheory.Limits.Presheaf looks like this:

@[reducible]
def functorToRepresentables (P : Cᵒᵖ ⥤ Type v₂) : P.Elementsᵒᵖ ⥤ Cᵒᵖ ⥤ Type (max v₁ v₂) :=
  (CategoryOfElements.π P).leftOp ⋙ yoneda ⋙ (Functor.whiskeringRight .. |>.obj uliftFunctor)

@[simps]
noncomputable def coconeOfRepresentable (P : Cᵒᵖ ⥤ Type v₂) :
    Cocone (functorToRepresentables P) where
  pt := P ⋙ uliftFunctor
  ι :=
    { app := fun x => {
        app := fun _ a => ⟨P.map a.down.op x.unop.2⟩
      }
    }

theorem coconeOfRepresentable_naturality {P₁ P₂ : Cᵒᵖ ⥤ Type v₂} (α : P₁ ⟶ P₂) (j : P₁.Elementsᵒᵖ) :
    (coconeOfRepresentable P₁).ι.app j ≫ α = -- Application type mismatch error for `α`
 ...

which is a bit unwieldy. But maybe doable!

[Joël Riou]

I have a draft branch where I fix this particular universe issue (which is quite painful to do). I will try to PR it soon.

[Emily Riehl]

Thanks @Joël Riou. Let us know if we can help. This is the last thing blocking the construction of the strict bicategory of quasi-categories.

[Joël Riou]

For the moment, do not hesitate to focus on the Type 0 case, and it should be easy to refactor the code afterwards.

[Joël Riou]

I have finally managed to make #27576 compile. (In particular, this generalizes the construction of singular homology to topological spaces in arbitrary universes.) It is still very much a draft, not at all ready for review.

[Joël Riou]

This PR should now be ready for review.

[Robin Carlier]

Will look at it. I was also interested in that result.