Zulip Chat Archive

Stream: new members

Topic: quotient of product


view this post on Zulip Kenny Lau (Jun 06 2019 at 19:08):

universes u v
variables (ι : Sort u) (β : ι  Sort v)
variables [c : Π x : ι, setoid (β x)]
include c

instance d : setoid (Π x, β x) :=
⟨λ f g,  x, f x  g x, sorry

example (f : Π x : ι, quotient (c x)) : quotient (d ι β) := sorry

view this post on Zulip Kenny Lau (Jun 06 2019 at 19:08):

Is it possible to have a sensible quotient on the product?

view this post on Zulip Chris Hughes (Jun 06 2019 at 19:12):

If the relation is true then this is almost choice, so I guess you have to use choice.

view this post on Zulip Reid Barton (Jun 06 2019 at 19:12):

Is this quotient.choice?

view this post on Zulip Reid Barton (Jun 06 2019 at 19:15):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/quotients.20and.20lifts.20for.20functions.20of.20arbitrary.20arity/near/150709555

view this post on Zulip Kenny Lau (Jun 06 2019 at 19:15):

oh thanks

view this post on Zulip Kenny Lau (Jun 07 2019 at 07:37):

@Reid Barton Does this mean we should always construct quotient of a product when we can, since it is intuitively stronger?


Last updated: May 08 2021 at 04:14 UTC