Commutative Diagram Widget

Stream: lean4

[Sina]

I am experimenting with the CommDiag widget by @Wojciech Nawrocki here: https://github.com/leanprover-community/mathlib4/pull/363
This is really awesome. Thanks for doing it.

Just wanted to report that in some examples the labeling of nodes (i.e. objects) are wrong. Perhaps, you have already noticed this in which case please ignore this message. Here is an example:

example {X Y Z : Type} {f g : X ⟶ Y} {k : Y ⟶ Y} {f' : Y ⟶ Z} :
  (f ≫ k) = g → ((f ≫ k) ≫ f') = (g ≫ 𝟙 Y ≫ f') := by
  withAlgebraDisplay
    intro h
    simp [h]
    rw  [← category.assoc' g (𝟙 Y) f']
    rw [category.comp_id' g]

In the bottom row of the following diagram objects Z and Y should be swapped.
Screen-Shot-2022-11-14-at-10.40.22-PM.png

[Wojciech Nawrocki]

Thank you for trying it out and for the report! I have not seen this before -- I will fix it. The visualization is in really early stages, so there will be many bugs; but reports are appreciated :) Of course there is another clear issue in that the nested compositions should be probably be expanded into their own arrows.

[František Silváši 🦉]

Whoa, this exists... alright this is brilliant. (Nevermind me, just a random comment.)