Naming of universal property lemmas

Stream: mathlib4

[Eric Wieser]

/poll Which of these is called lift_comp_ι?

• lift (g ∘ ι) = g
• (lift f) ∘ ι = f

[Eric Wieser]

And of course the more important question, what should the other one be called?

[Eric Wieser]

We have precedent here, but the precedent is to call the other one ι_comp_lift, which is definitely not a reasonable reading of the naming guide.

[Aaron Liu]

can you give some examples?

[Aaron Liu]

I'm having trouble inferring the types in lift (g ∘ ι) = g

[Aaron Liu]

oh I figured it out

[Eric Wieser]

g : BigHom (F X) Y, f : LittleHom X Y, ι : LittleHom X (F X)

[Eric Wieser]

I guess strictly speaking (lift f) ∘ ι = f is actually (lift f).toLittleHom.comp ι = f, which maybe solves the naming issue

[Kenny Lau]

lift_app_comp_ι would be the other one :smile:

[Aaron Liu]

Eric Wieser said:

I guess strictly speaking (lift f) ∘ ι = f is actually (lift f).toLittleHom.comp ι = f, which maybe solves the naming issue

Strictly speaking lift (g ∘ ι) is actually lift (g.toLittleHom.comp ι)

[Aaron Liu]

but sometimes LittleHom and BigHom are the same type

[Michael Stoll]

lift__comp_ι and lift_comp__ι? :grinning_face_with_smiling_eyes:

[Eric Wieser]

lift_comp_ι and comp_lift_ι, ignoring the infix-ness?