graphical widget example

Stream: lean4

[Kevin Buzzard]

I'm helping to port directed systems. @Wojciech Nawrocki what can you make of the definition

/-- A directed system is a functor from a category (directed poset) to another category. -/
class DirectedSystem (f : ∀ i j, i ≤ j → G i → G j) : Prop where
  map_self' : ∀ i x h, f i i h x = x
  map_map' : ∀ {i j k} (hij hjk x), f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x

using your commutative algebra widget? When you read it like this, map_map' is incomprehensible.

[Wojciech Nawrocki]

Hm, so all the examples I wrote down so far only support pointless equalities but there is no a priori reason why pointwise equations quantified over the points (like x here) couldn't be displayed as well. Is there any specific way in which you'd like to display this, other than just the one triangle f i j hij ≫ f j k hjk = f i k (le_trans hij hjk)?

[Kevin Buzzard]

Certainly a triangle would be much better than what we have currently!