## Stream: new members

### Topic: quot of fintype is fintype?

#### 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?

#### 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)

#### Vaibhav Karve (Mar 22 2020 at 21:48):

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

#### Kenny Lau (Mar 22 2020 at 21:48):

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

#### Kevin Buzzard (Mar 22 2020 at 21:49):

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

#### Kevin Buzzard (Mar 22 2020 at 21:50):

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

#### Kenny Lau (Mar 22 2020 at 21:50):

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

#### Kevin Buzzard (Mar 22 2020 at 21:50):

and I can do it in both cases!

#### Kenny Lau (Mar 22 2020 at 21:51):

but fintype is data

#### Kevin Buzzard (Mar 22 2020 at 21:57):

I just have some if then else, right?

#### 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

#### 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

#### 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