name for, and question about, computational principle

Stream: general

[Kevin Buzzard]

In section 11.4 of TPIL they talk about quotients. The computational principle is introduced with its rfl proof.

theorem thm : quot.lift f h (quot.mk r a) = f a := rfl

The theorem is given the unilluminating name of thm. I'm rolling my own quotient structure. Does this theorem have a canonical name? Furthermore, I realise that I also want a variant for my structure where f is Prop-valued and the theorem states

theorem thm' : quot.lift f h (quot.mk r a) ↔ f a

Does this theorem have a canonical name?

---

The question is this: In section 3.7 of the reference manual they define abstract definitional equality, and then mention (right near the end) that Lean's procedure is "more conservative". But in the formal definition of definitional equality this computational principle for quot is never mentioned. So it seems to me that Lean's procedure is less conservative in this instance.

[Chris Hughes]

I think it might be called quot.lift_beta

[Kevin Buzzard]

Oh indeed! I just looked in core lean and lo and behold it's not called thm after all :-) So should we call ours lift_beta? Johan called it lift_eq which I thought sounded much better.