terminal.comp_from_assoc

Stream: mathlib4

[Charlie Conneen]

In CategoryTheory.Limits.Shapes.Terminal:

@[simp]
theorem terminal.comp_from [HasTerminal C] {P Q : C} (f : P ⟶ Q) :
    f ≫ terminal.from Q = terminal.from P := by
  simp [eq_iff_true_of_subsingleton]

Should this be tagged as reassoc? (Similarly for initial.to_comp)

[Charlie Conneen]

Admittedly it's probably not often that one is mapping out of the terminal object, but this has proven to be a significant use case.

[Notification Bot]

This topic was moved here from #mathlib4 > terminal.comp_from by Charlie Conneen.

[Andrew Yang]

Most probably yes.

[Charlie Conneen]

It seems that initial.to_comp_assoc does not need to be a simp lemma. I have opted to simply not add the reassoc tag to initial.to_comp. PR is here: #21527

[Andrew Yang]

An assoc version of initial.to_comp might still be useful though. Perhaps add the assocbut without taging the assoc as simp? (You can achieve this by @[simp, reassoc] instead of @[reassoc (attr := simp)])

[Charlie Conneen]

Ah, sure. Thanks for input.