broken symmetric instance on simplicial sets

Stream: Infinity-Cosmos

[Emily Riehl]

A mathlib update broke something in our repository that I haven't had a chance to chase down yet:

noncomputable instance : MonoidalClosed SSet where
  closed A := {
    rightAdj := (sHomFunctor _).obj ⟨A⟩
    adj := FunctorToTypes.adj _
  }

noncomputable instance : SymmetricCategory SSet := inferInstance

Now the infer instance fails. Does anyone know what might be going on?

[Aaron Liu]

#mwe would be great

[Aaron Liu]

Right now I'm looking at #24399

[Andrew Yang]

It depends on how the BraidedCategory instance on SSet is defined. If it was ChosenFiniteProducts, then BraidedCategory is unbundled from it so you would need to do docs#CategoryTheory.BraidedCategory.ofChosenFiniteProducts by hand