replacing `category_theory.discrete` with a structure

Stream: general

[Scott Morrison]

We've often found with typeclass synonyms, if they are semireducible (the default setting) often Lean gets confused. This seems to be happening with category_theory.discrete, and making working category_theory.has_shift quite painful.

(Recall we model shift functors on a category as a monoidal functor from a monoid A (thought of as a discrete monoidal functor) to C \func C (again thought of as a monoidal category).)

I've been experimenting with replacing category_theory.discrete with a custom structure. It's been a fair bit of work, but I'm hopeful it will be helpful, and perhaps is mostly there. However there are a few files where I've got stuck fixing the errors, and I'd like to ask for help. I'm going to shamelessly ping people here in the hope that they could have a look at files they are experts on. :-) This is all in branch#discrete_structure.

• @Adam Topaz, src/category_theory/limits/shapes/multiequalizer.lean
• @Yuma Mizuno and @Markus Himmel, src/category_theory/bicategory/coherence.lean and src/category_theory/monoidal/coherence.lean
• @Markus Himmel or @Jakob von Raumer, src/category_theory/limits/shapes/biproducts.lean
• @Praneeth Kolichala, src/category_theory/category/Groupoid.lean.

In each case, the request is just to see if you can make the red squiggles go away! In some of these files I've made partial progress, in others, not so much. :-)

[Adam Topaz]

I fixed multiequalizer.lean. (and pushed to the same branch)

[Scott Morrison]

Thank you!

[Jakob von Raumer]

I had a look at biproducts.lean. The issue can be solved by e.g. in ... manually rewriting the elements in J to projections from discrete J:

lemma biproduct.map_eq_map' {f g : J → C} [has_biproduct f] [has_biproduct g]
  (p : Π b, f b ⟶ g b) : biproduct.map p = biproduct.map' p :=
begin
  ext j j',
  have : j = (⟨j⟩ : discrete J).as, { refl }, rw this,
  have : j' = (⟨j'⟩ : discrete J).as, { refl }, rw this,
  simp only [discrete.nat_trans_app, limits.is_colimit.ι_map, limits.is_limit.map_π, category.assoc,
    ←bicone.to_cone_π_app, ←biproduct.bicone_π, ←bicone.to_cocone_ι_app, ←biproduct.bicone_ι],
  simp only [biproduct.bicone_ι, biproduct.bicone_π, bicone.to_cocone_ι_app, bicone.to_cone_π_app],
  dsimp,
  rw [biproduct.ι_π_assoc, biproduct.ι_π],
  split_ifs,
  { subst h, rw [eq_to_hom_refl, category.id_comp], erw category.comp_id, },
  { simp, },
end

[Jakob von Raumer]

Pushed a fix for this, by not using @[simps] on bicone.to_cone and bicone.to_cocone, and instead stating the simp lemma in terms of J instead of discrete J.

[Jakob von Raumer]

The errors further down are about b.to_bicone.to_cone and b.to_cone not being of the same type anymore

[Jakob von Raumer]

Jakob von Raumer said:

The errors further down are about b.to_bicone.to_cone and b.to_cone not being of the same type anymore

Which in turn is an issue of whether we want to use discrete walking_pair or walking_pair, maybe using discrete to redefine the latter.

[Scott Morrison]

Thanks, based on this hint I think I've got biproducts sorted now.

[Scott Morrison]

I pushed the remaining fixes to biproducts, yay. Still have't solved the problems in the coherence theorems, or Groupoid, but will hopefully get back to these (unless someone else does :-).

[Markus Himmel]

I fixed the errors in the monoidal coherence theorem. Two leamms need to be moved and some general cleanup is needed, but I won't have time for that until next week.

[Scott Morrison]

Thanks Markus. @Yuma Mizuno, any chance you could have a look at branch#discrete_structure, in particular src/category_theory/bicategory/coherence.lean?

[Yuma Mizuno]

@Scott Morrison I got stuck once, but I will try again today.

[Junyan Xu]

I wonder why docs#category_theory.discrete.functor isn't changed to use eq_to_hom? The current definition using tactics seems bad since it results in the following convoluted term involving eq.rec:

category_theory.discrete.functor F = {obj := F,
map := λ (X Y : category_theory.discrete I) (f : X ⟶ Y),
  ulift.cases_on f (λ (f : plift (X = Y)),
    f.cases_on (λ (f : X = Y), f.dcases_on (λ (H_1 : Y = X),
      eq.rec (λ (f : X = X) (H_2 : f == _), 𝟙 (F X)) _ f) _ _)), map_id' := _, map_comp' := _}

[Scott Morrison]

@Junyan Xu do you want to try it out? Feel free to experiment on this branch!

[Yuma Mizuno]

I removed errors in src/category_theory/bicategory/coherence.lean. I did one cheating though, redefining locally_discrete C as a type class synonyms of C.

[Praneeth Kolichala]

@Scott Morrison I fixed Groupoid.lean, but I added a few helper lemmas in limits/shapes/products.lean which need to be dualized (should be easy, or I can do them later, but I'm busy now).