quot.ind

Stream: general

[Kevin Buzzard]

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]

because function.surjective hasn't been defined

[Kenny Lau]

the four constants of quot are all initiated in core

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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