# Zulip Chat Archive

## Stream: new members

### Topic: Is quotient special?

#### Walter Moreira (May 18 2020 at 02:59):

Is there something special in the `quot`

construction in Lean kernel? I tried to reproduce my own quotient following the declarations in https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients but I don't get the same reduction as the original construction. What is it missing?

```
universes u v
variables α β : Type
variable r : α → α → Prop
variable a : α
variable f : α → β
variable h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂
-- same declarations as TPiL changing quot by my_quot
constant my_quot : Π {α : Sort u}, (α → α → Prop) → Sort u
constant my_quot.mk :
Π {α : Sort u} (r : α → α → Prop), α → my_quot r
axiom my_quot.ind :
∀ {α : Sort u} {r : α → α → Prop} {β : my_quot r → Prop},
(∀ a, β (my_quot.mk r a)) → ∀ (q : my_quot r), β q
constant my_quot.lift :
Π {α : Sort u} {r : α → α → Prop} {β : Sort u} (f : α → β),
(∀ a b, r a b → f a = f b) → my_quot r → β
axiom my_quot.sound :
∀ {α : Type u} {r : α → α → Prop} {a b : α},
r a b → my_quot.mk r a = my_quot.mk r b
#reduce quot.lift f h (quot.mk r a) -- f a
#reduce my_quot.lift f h (my_quot.mk r a) -- itself
```

#### Bryan Gin-ge Chen (May 18 2020 at 03:02):

Yes, it is special. It gets introduced in core Lean with a special keyword: https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L151

What you're missing is the special reduction rule mentioned there.

#### Yury G. Kudryashov (May 18 2020 at 03:02):

Yes, reduction rule for `lift`

is implemented in C++.

#### Walter Moreira (May 18 2020 at 03:13):

So, is my mental model correct if I think on `quot.lift f h (quot.mk r a) ~~> f a`

as an "extra" rule at the same level with the $\beta$, $\eta$, etc. reductions?

#### Mario Carneiro (May 18 2020 at 03:22):

yes

#### Mario Carneiro (May 18 2020 at 03:22):

This exact rule is mentioned at https://leanprover.github.io/reference/expressions.html#axioms

#### Walter Moreira (May 18 2020 at 03:25):

That was useful. Thank, folks!

Last updated: May 14 2021 at 12:18 UTC