Refactoring `WithTerminal`

Stream: mathlib4

[Robin Carlier]

Now that the last entry (#25744) in the "joins of categories" series have been merged, I don’t think there is much benefit of having WithTerminal and WithInitial as separate constructions: they are joins of C with Discrete PUnit.
Almost all constructions for WithTerminal (except the identification between functors out of joins with suitable comma categories) are available as Join construction, so I would like to suggest redefining WithTerminal (and the relevant objects) as an abbrev for C ⋆ Discrete PUnit.{1}. Any objections?

[Yaël Dillies]

How does that interact with replacing docs#CategoryTheory.Limits.WidePullbackShape with WithTerminal?

[Robin Carlier]

Do you have a wip PR doing this?

I don’t see it being much harder. Joins have nice universal properties to construct and characterize up to iso functors out of them, there’s an induction principle for maps, and WithTerminal.lift (arguably the only way one should define a functor from a WithTerminal) should remain the same.

I was thinking of also doing

@[match_pattern]
abbrev star : WithTerminal C := Join.right ⟨.unit⟩
@[match_pattern]
abbrev of (c : C) : WithTerminal C := Join.left c

so that match statement on objects can literally remain the same.

So tl;dr I don’t think this would have much interaction/negative impact.

[Robin Carlier]

(For match on morphisms, they’d be almost the same but aesop has slight trouble using the induction principle for maps, so I feel it’s better anyway in contsructions to go through the provided "universal properties" constructors rather than direct constructions).

[Yaël Dillies]

Robin Carlier said:

Do you have a wip PR doing this?

No, I was waiting on @Moisés Herradón Cueto's work to hit mathlib fully before starting such a refactor

[Bhavik Mehta]

I agree that both Robin's and Yaël's refactors are good ideas here, and that they can (and should) coexist.