Zulip Chat Archive

Stream: mathlib4

Topic: ConeMorphism.Hom

Jakob von Raumer (Sep 13 2023 at 11:08):

Why is ConeMorphism.Hom capitalized?

Ruben Van de Velde (Sep 13 2023 at 11:57):

Likely by accident

Scott Morrison (Sep 13 2023 at 14:12):

Mathport accident, that became entrenched. I'll happily hit merge on a fix. :-)

Jakob von Raumer (Sep 13 2023 at 15:51):

Will fix

Eric Wieser (Sep 17 2023 at 10:19):

It's a type, right?

Eric Wieser (Sep 17 2023 at 10:19):

docs#CategoryTheory.Limits.ConeMorphism

Jakob von Raumer (Sep 18 2023 at 07:50):

#7176

Last updated: Dec 20 2023 at 11:08 UTC