should we shutdown the local "mathlib" folder?

Stream: Infinity-Cosmos

[Emily Riehl]

Thanks to work of @Pietro Monticone and @Patrick Massot it's now possible to link to mathlib definitions in the blueprint. Previously these links were broken, which is why we copied the most relevant files from the AlgebraicTopology folder into the local Mathlib folder (the one under the InfinityCosmos folder, next to the ForMathlib folder).

Now I'm thinking it probably makes sense to prune these out and move everything that only exists in this repository into the ForMathlib folder. This folder will contain two types of files:
(i) totally new files, with a name that doesn't currently exist in mathlib, which have no mathlib parallel. One example is the current "InfinityCosmos/Basic.lean".
(ii) files which share a name with an existing mathlib file, that will start by importing that mathlib file, and then continuing with new content. Eg our current "AlgebraicTopology/SimplicialCategory/Basic.lean" adds a few lines to the current mathlib version:

noncomputable instance : SimplicialCategory SSet where
  toEnrichedCategory := inferInstanceAs (EnrichedCategory (_ ⥤ Type _) (_ ⥤ Type _))
  homEquiv K L :=
    letI e : (K ⟶ L) ≃ (K ⊗ 𝟙_ SSet ⟶ L) :=
      ⟨fun f => (ρ_ _).hom ≫ f, fun f => (ρ_ _).inv ≫ f, by aesop_cat, by aesop_cat⟩
    e.trans (Functor.homObjEquiv _ _ _).symm |>.trans (Functor.functorHomEquiv K L (𝟙_ SSet)).symm
  homEquiv_id := by aesop_cat
  homEquiv_comp := by aesop_cat

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

noncomputable instance : SymmetricCategory SSet := inferInstance
-- instance : HasBinaryProducts SSet := by infer_instance

/-- The monoidal structure given by the `ChosenFiniteProducts` has good definitional properties,
like the following: -/
example (R S : SSet) (n : SimplexCategory) : (R ⊗ S).obj ⟨n⟩ = (R.obj ⟨n⟩ × S.obj ⟨n⟩) := rfl

Within the "ForMathlib" folder, we'd replicate the relevant portions of Mathlib directory structure, like we do now, so that it will be clear where everything belongs. It won't necessarily be obvious from the file tree whether something is an extension of a current mathlib file or a totally new file, except when you look at the imports, the mathlib extension files will be very easy to spot (as they import the rest of themselves).

[Emily Riehl]

The advantage of this new structure is it will make it clearer what is in mathlib and what stuff we might want to PR. (@Kim Morrison suggested that we do this regularly for the stuff that's likely to be of broader interest, rather than have new content build up endlessly.) It will also solve issues with duplicate imports that have tripped me up at various times.

[Emily Riehl]

The disadvantage is this reorganization would be very disruptive to anyone who is currently working on a branch of the infinity-cosmos repository. Are there any branches out there that I'm not aware of?

[Pietro Monticone]

For those interested in the "fix" that nobody seems to know why it worked :sweat_smile:, here is the topic where we discussed it: #general > doc-gen not finding Mathlib declarations.