subtypes v sets

Stream: general

[Kevin Buzzard]

I have U : set alpha and I want to make a Pi type which morally is \Pi P : U, (some function of P)

[Kevin Buzzard]

I went for \Pi P : {u : alpha // U u}, ...

[Kevin Buzzard]

and now I am constantly running into v \in U which I want to do my Pi
stuff to

[Kevin Buzzard]

meh I guess I just shouldn't be considering "elements of U" I should just be avoiding the set notation completely now

[Andrew Ashworth]

if you want to stay with sets, you could use the set image lemmas

[Andrew Ashworth]

but definitely type theory notation is more natural to work in

[Mario Carneiro]

I have U : set alpha and I want to make a Pi type which morally is \Pi P : U, (some function of P)

Did you actually try \Pi P : U, (some function of P)? That should work because of coercions

[Kevin Buzzard]

No I didn't :-) I know that if I'd tried this, I would have ended up not knowing what the type of P actually was, at least initially. Probably what you're saying is that if I'd tried it, it would have unfolded into what I actually used. More and more I am deciding not to use coercions or type classes because I realise that rather than using them and then struggling later it is easier for me to just do all the work myself. I guess what I'm saying is that initially things like coercions and the type class system were complete mysteries to me and I could see them working in simple cases and failing in more complex ones and didn't really understand enough to know how to make them work for me. Now I've decided to do all coercions myself, and of course now I understand what's going on much better. The next phrase will be me attempting to use these tools again, but this time knowing how to use them properly.

[Chris Hughes]

@Kevin Buzzard I just wrote some docs about this, which I PRed to your WIP docs.

[Patrick Massot]

@Chris Hughes your doc on set-like stuff is awesome. I added some comments (but I guess Kevin needs to allow them before you can see them). Then I think this should go straight to mathlib in the theories folder (with a link in https://github.com/leanprover/mathlib/blob/master/docs/theories.md)

[Chris Hughes]

The main downside I can see to the Pi version, is if you ever wanted to prove the function is injective or has an inverse. No idea if you'd ever want to do that.

[Kevin Buzzard]

In my context I don't think I'll ever want to do this.