Zulip Chat Archive

Stream: new members

Topic: quot of fintype is fintype?


view this post on Zulip Vaibhav Karve (Mar 22 2020 at 21:37):

In type theory, is not the quot of a fintype a fintype?

example (A) [fintype A] (r : A -> A -> Prop) : fintype (quot r) := sorry

I found that there is a quotient.fintype

quotient.fintype :
  Π {α : Type u_1} [_inst_1 : fintype α] (s : setoid α) [_inst_2 : decidable_rel has_equiv.equiv],
    fintype (quotient s)

but that only works for decidable equivalence relations. What about general relations?

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 21:47):

rofl this is just the sort of nonsense where someone will come along and say it's not true :-) (or not provable or whatever)

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 21:48):

My set-theory intuition says it should be true :slight_smile:

view this post on Zulip Kenny Lau (Mar 22 2020 at 21:48):

let A be bool and r 0 1 be true iff the Riemann Hypothesis holds

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 21:49):

Still looks finite to me -- just check in both cases.

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 21:50):

But don't press me on the cardinality...

view this post on Zulip Kenny Lau (Mar 22 2020 at 21:50):

now you are tasked with producing a full list of elements in the quotient without duplicates

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 21:50):

and I can do it in both cases!

view this post on Zulip Kenny Lau (Mar 22 2020 at 21:51):

but fintype is data

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 21:57):

I just have some if then else, right?

view this post on Zulip Mario Carneiro (Mar 23 2020 at 02:43):

Isn't your if then else going to rely on decidability of the relation? (Even if the proof of this is "because I'm a mathematician".) If you assume classical, then decidable equivalence relations are all equivalence relations

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:10):

Yeah I'm well aware of the situation we're in, however it doesn't stop me laughing at constructivism as a consequence

view this post on Zulip Vaibhav Karve (Mar 23 2020 at 12:45):

I see. I think in my case I will use a quotient then. I want my definition to carry data -- so I am avoiding classical reasoning as much as possible.


Last updated: May 14 2021 at 03:27 UTC