quot.ind in metatheory paper

Stream: general

[Floris van Doorn]

In Section 2.7 of Mario's metatheory of Lean paper, I'm missing the fact that quot.ind is a axiom in Lean. Is this an omission, or is there an implicit claim here that quot.ind is derivable from the other constants/axioms?

[Gabriel Ebner]

I'm pretty sure that quot.ind is only derivable if the underlying type α is empty.

[Floris van Doorn]

That is too strong. You can at least prove it for unit by using that x = unit.star for every x : unit (and therefore quot.mk x = quot.mk unit.star). And I suspect that (classically) you might be able to do something when α is fin n, for example.

[Floris van Doorn]

oh wait, maybe I'm mentally already using quot.indhere.

[Floris van Doorn]

Oh yes, you're right. If α is nonempty, say z : α, and r : α -> α -> Prop then I can define

quot' α r := option (quot α r)
quot'.mk r x := some (quot.mk r x)
quot'.lift β f h (some x) := quot.lift β f h x
quot'.lift β f h none := f z

and then quot' satisfies the same rules as quot, including the reduction rule, but excluding quot.ind

[Floris van Doorn]

Also, the paper claims/proves that using only the inductive types empty psigma psum ulift nonempty W eq acc we can construct all others. If we remove acc from this list, so we only have the other 7 inductive types, do we know whether the ("ideal") definitional equality in the resulting system decidable?

[Mario Carneiro]

@Floris van Doorn The reasoning behind only considering quot.sound an axiom and ignoring the others is that the others taken together are conservative, because we can take quot A = A and then all the axioms are valid except quot.sound. quot.ind is valid because id is surjective

[Mario Carneiro]

That said, I don't think this is common practice in logic, I should probably just call them all axioms

[Mario Carneiro]

I don't know if removing acc makes defeq decidable, but my guess is yes. Of course the counterexample in the paper uses acc essentially

[Floris van Doorn]

@Mario Carneiro I don't care about which of them you call constants and which you call axioms, my point is that you forgot to mention quot.ind in the paper (in the latest release and on the master branch). You only mention quot.lift as elimination principle.

[Mario Carneiro]

Now I forget if quot.rec or quot.lift + quot.ind were used internally by lean

[Floris van Doorn]

quot.rec is defined in terms of quot.lift + quot.ind.

[Mario Carneiro]

ok, I'll update the paper

[Floris van Doorn]

The issue with the nontransitivity of algorithmic definitional equality using quot is only because if α : Sort u then @quot α r : Sort u, right? If we alternatively defined @quot α r to be in Sort (max u 1) (which would make more sense, compared to inductive types), then the nontransitivity using quotients goes away, right?

[Floris van Doorn]

thanks!

[Mario Carneiro]

yes

[Mario Carneiro]

All of the known examples of failure of transitivity involve some kind of subsingleton elimination, where an inductive type in Prop recurses over Type. So it is reasonable to conjecture that without acc and with quot out of Prop the algorithmic equality becomes transitive, and so coincides with ideal defeq which becomes decidable.