Proof-irrelevant simps

Stream: mathlib4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The @[simps!] annotation on docs#CategoryTheory.Over.homMk generates a rather weird lemma docs#CategoryTheory.Over.homMk_right_down_down which equates two proofs of equality. This is completely trivial by proof irrelevance / UIP. Does this lemma actually serve a purpose, or is it a bug in @[simps]?

[Kim Morrison]

Sounds like a problem with simp.

[Kim Morrison]

You can probably disable it with @[simps -right_down_down] or some similar syntax, just to double check. But seems very unlikely.