quot of fintype is fintype?

Stream: new members

[Vaibhav Karve]

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?

[Kevin Buzzard]

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

[Vaibhav Karve]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

and I can do it in both cases!

[Kenny Lau]

but fintype is data

[Kevin Buzzard]

I just have some if then else, right?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Vaibhav Karve]

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.