help fixing broken files after mathlib bump

Stream: Infinity-Cosmos

[Emily Riehl]

The local version of mathlib in the infinity-cosmos repository was very out of date; thanks to @Pietro Monticone for helping me update it.

Unfortunately now two files are broken.

[Emily Riehl]

I'm hoping @Julian Komaromy can fix the issues in his Horn file. There seems to be an off by one error here

def multispanIndex : Limits.MultispanIndex J SSet where
  left  _ := Δ[1]
  right _ := Δ[2]
  fst p := stdSimplex.map (δ (Fin.pred p.val.2.val (Fin.ne_zero_of_lt p.property)).castSucc)
  snd p := stdSimplex.map (δ p.val.1.val)

as well as in the other multispanIndex.

[Emily Riehl]

The other errors are in @Daniel Carranza's MonoidalProdCat file. They are all failures to infer instances of MonoidalCatStruc. This should be easy to fix but I'm not good at handling errors of this type.

[Emily Riehl]

The first is here:

variable (V : Type u₁) [Category.{v₁} V] [MonoidalCategory V]
variable (C : Type u₂) [EnrichedCategory V C]
variable (D : Type u₃) [EnrichedCategory V D]

-- Helper lemma for Bifunc.mk
lemma comp_tensor_comp_eq_comp_mid_left_right {a b c d e : C} :
    ((eComp V a b c) ⊗ (eComp V c d e)) ≫ eComp V a c e =
      (α_ _ _ _).hom ≫ _ ◁ (α_ _ _ _).inv ≫ _ ◁ ((eComp V b c d) ▷ _) ≫ _ ◁ (eComp V b d e) ≫
        eComp V a b e := by
  rw [← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc]
  simp only [Category.assoc, e_assoc, MonoidalCategory.whiskerLeft_comp]
  rw [← associator_naturality_right_assoc, e_assoc', ← tensorHom_def'_assoc]

The first of several similar error messages is

failed to synthesize
  MonoidalCategoryStruct (((a ⟶[V] b) ⊗ b ⟶[V] c) ⟶ a ⟶[V] c)

[Emily Riehl]

This refers to various structures defined in mathlib:

class EnrichedCategory (C : Type u₁) where
  /-- `X ⟶[V] Y` is the `V` object of morphisms from `X` to `Y`. -/
  Hom : C → C → V
  /-- The identity morphism of this category -/
  id (X : C) : 𝟙_ V ⟶ Hom X X
  /-- Composition of two morphisms in this category -/
  comp (X Y Z : C) : Hom X Y ⊗ Hom Y Z ⟶ Hom X Z
  id_comp (X Y : C) : (λ_ (Hom X Y)).inv ≫ id X ▷ _ ≫ comp X X Y = 𝟙 _ := by cat_disch
  comp_id (X Y : C) : (ρ_ (Hom X Y)).inv ≫ _ ◁ id Y ≫ comp X Y Y = 𝟙 _ := by cat_disch
  assoc (W X Y Z : C) : (α_ _ _ _).inv ≫ comp W X Y ▷ _ ≫ comp W Y Z =
    _ ◁ comp X Y Z ≫ comp W X Z := by cat_disch

@[inherit_doc EnrichedCategory.Hom] notation3 X " ⟶[" V "] " Y:10 => (EnrichedCategory.Hom X Y : V)

variable {C : Type u₁} [EnrichedCategory V C]

/-- The `𝟙_ V`-shaped generalized element giving the identity in a `V`-enriched category.
-/
def eId (X : C) : 𝟙_ V ⟶ X ⟶[V] X :=
  EnrichedCategory.id X

/-- The composition `V`-morphism for a `V`-enriched category.
-/
def eComp (X Y Z : C) : ((X ⟶[V] Y) ⊗ Y ⟶[V] Z) ⟶ X ⟶[V] Z :=
  EnrichedCategory.comp X Y Z

[Julian Komaromy]

Emily Riehl said:

I'm hoping Julian Komaromy can fix the issues in his Horn file. There seems to be an off by one error here

def multispanIndex : Limits.MultispanIndex J SSet where
  left  _ := Δ[1]
  right _ := Δ[2]
  fst p := stdSimplex.map (δ (Fin.pred p.val.2.val (Fin.ne_zero_of_lt p.property)).castSucc)
  snd p := stdSimplex.map (δ p.val.1.val)

as well as in the other multispanIndex.

Unfortunately, from taking a quick look at it, the definition of the multispan itself seems to be wrong, so I don't immediately see a one-liner fix. I will take a closer look over the weekend.

[Julian Komaromy]

@Emily Riehl I pushed a new PR providing a (somewhat temporary?) fix for the build issues in Horn.lean

[Emily Riehl]

Update: today @Daniel Carranza and I were able to fix everything that was broken. The error was caused by some changes to notation for tensor products of morphisms in monoidal categories and theorems about this.