## Stream: new members

### Topic: Is a namespace a type?

#### Lars Ericson (Dec 11 2020 at 16:49):

Regarding this:

namespace quot
variable {β : quot r → Sort v}


It appears that a namespace defines a class. Is that correct?

#### Eric Wieser (Dec 11 2020 at 16:50):

No, it just shares a name with a type

#### Kevin Buzzard (Dec 11 2020 at 16:51):

You can read about namespaces in #tpil, a book which you are probably now in a position to get to the end of. Your code doesn't run for me. quot is already a thing in core Lean -- is this what is confusing you?

#### Eric Wieser (Dec 11 2020 at 16:51):

docs#quot should be the definition

#### Eric Wieser (Dec 11 2020 at 16:52):

Huh, I was expecting a meta constant or something

#### Kevin Buzzard (Dec 11 2020 at 16:55):

go to definition also fails in VS Code

#### Reid Barton (Dec 11 2020 at 16:57):

quot and its associated constants are magically declared to exist by the kernel

#### Reid Barton (Dec 11 2020 at 16:57):

there's some command which triggers their construction which I forget

#### Kevin Buzzard (Dec 11 2020 at 16:57):

init_quotient in core.lean

#### Kevin Buzzard (Dec 11 2020 at 16:58):

/-
Initialize the quotient module, which effectively adds the following definitions:

constant quot {α : Sort u} (r : α → α → Prop) : Sort u

constant quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : quot r

constant quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → eq (f a) (f b)) → quot r → β

constant quot.ind {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} :
(∀ a : α, β (quot.mk r a)) → ∀ q : quot r, β q

Also the reduction rule:

quot.lift f _ (quot.mk a) ~~> f a

-/
init_quotient


#### Adam Topaz (Dec 11 2020 at 16:59):

Will quot still be magic in lean4?

#### Kevin Buzzard (Dec 11 2020 at 17:10):

prelude

init_quotient


gives the rather tasty error message

failed to initialize quot module, environment does not have 'eq' type


One could maybe redefine eq and prove false somehow?

prelude

universe u

def Prop := Sort 0

inductive false : Prop

def eq : Π {α : Sort u}, α → α → Prop := λ α a b, false
/-
equation compiler failed to create auxiliary declaration 'eq.equations._eqn_1'
nested exception message:
unknown declaration 'eq.refl'
-/


kind of annoying. I'm not sure what the rules are in prelude

#### Reid Barton (Dec 11 2020 at 17:13):

I wonder why it wanted to use the equation compiler

#### Reid Barton (Dec 11 2020 at 17:13):

What if you just make an inductive type like eq but empty

#### Eric Wieser (Dec 11 2020 at 17:24):

Found this nice error message while trying that:

https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/src/kernel/quotient/quotient.cpp#L63

#### Eric Wieser (Dec 11 2020 at 17:24):

Looks like it was meant to say "unexpected" not "expected"?

#### Reid Barton (Dec 11 2020 at 17:25):

nope, Lean is just onto you and your tricky ways

#### Eric Wieser (Dec 11 2020 at 17:26):

Actually def Prop breaks it

#### Eric Wieser (Dec 11 2020 at 17:26):

It requires it to be notation

#### Eric Wieser (Dec 11 2020 at 17:27):

But yes, check_eq_type looks fairly robust

#### Lars Ericson (Dec 11 2020 at 17:59):

Thanks for the clarification. So:

static environment init_quotient_cmd(parser & p) {
return module::declare_quotient(p.env());
}

namespace hidden
universes u v
constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u
end hidden


#### Lars Ericson (Dec 11 2020 at 20:33):

The application was that I was trying to trace out the types involved in a couple of representations of the set {0,1,2}, and quot came up as a blank spot, but that's OK. Here is the picture I came up with:
Screenshot-from-2020-12-11-15-32-05.png

#### Eric Wieser (Dec 11 2020 at 20:39):

Lars, if you like dependency graphs about lean, you might find https://observablehq.com/@eric-wieser/lean-ga-imports interesting

#### Chris B (Dec 11 2020 at 23:29):

@Lars Ericson

It also adds quot.mk, quot.lift, and quot.ind. They get assembled 'by hand' and then added to the environment without any checks as soon as the eq inductive has been admitted. If you print an export file from Lean 3, it will be a couple of name declarations, an #IND for eq, and then just #QUOT which tells the verifier to add the quotient stuff to the environment.

This file has comments with lean annotations showing what's actually being put together.
https://github.com/ammkrn/nanoda_lib/blob/master/src/quot.rs

#### Lars Ericson (Dec 11 2020 at 23:46):

@Eric Wieser that's really great visualization, thanks.

Last updated: May 15 2021 at 02:11 UTC