# Zulip Chat Archive

## Stream: general

### Topic: name for, and question about, computational principle

#### Kevin Buzzard (Mar 25 2019 at 14:22):

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 (Mar 25 2019 at 14:26):

I think it might be called `quot.lift_beta`

#### Kevin Buzzard (Mar 25 2019 at 14:32):

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.

Last updated: May 12 2021 at 04:19 UTC