Zulip Chat Archive

Stream: general

Topic: quot.ind


Kevin Buzzard (Aug 01 2018 at 10:11):

Am I right in thinking that quot.ind is logically equivalent to function.surjective (quot.mk r)? It's simply the universal property of a surjection. I am never 100% sure about these things because of computability or constructability or efficiency or whatever, but, assuming I've not made a slip, why do the CS guys choose quot.ind over the surjection statement? If beta were allowed to take values in Type then there would be some constructivity issues I guess, but because it's Prop aren't they exactly the same? Is it simply that quot.ind turns out to be more useful than the surjectivity statement in practice or is there something else going on?

Kenny Lau (Aug 01 2018 at 10:11):

because function.surjective hasn't been defined

Kenny Lau (Aug 01 2018 at 10:12):

the four constants of quot are all initiated in core

Mario Carneiro (Aug 01 2018 at 10:14):

Yes, quot.ind and quot.exists_rep are equivalent. Induction principles are preferred for axiomatics since they don't have any prerequisite definitions

Kevin Buzzard (Aug 01 2018 at 10:37):

I guess one could have simply spelled out the definition of surjection. I don't quite understand Mario's answer -- what is an "induction principle"? I only ever learnt one and that was about the natural numbers. Aah. Presumably in this context it means "something which constructs a map from the type we're talking about to Prop". OK. I see. Thanks!

Mario Carneiro (Aug 01 2018 at 10:40):

"induction principle" is often used synonymously with "recursor" in lean terminology

Mario Carneiro (Aug 01 2018 at 10:40):

Usually an induction principle has a motive that has a target in Prop though


Last updated: Dec 20 2023 at 11:08 UTC