Zulip Chat Archive

Stream: new members

Topic: quotient of product

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

Kenny Lau (Jun 06 2019 at 19:08):

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

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.

Reid Barton (Jun 06 2019 at 19:12):

Is this quotient.choice?

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

Kenny Lau (Jun 06 2019 at 19:15):

oh thanks

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: Dec 20 2023 at 11:08 UTC