I am interested in what the potential pathologies are that may arise from axiomatically adding quotient types to Coq. The way it's currently implemented in the coq-HoTT library using private modules and adjoining new computation rules seems sensible to me. This also seems to be the solution favored by @Gaëtan Gilbert in this discussion - https://github.com/coq/coq/issues/10871

Are there any problems that arise with this implementation? I guess it should break canonicity (?) because you're axiomatically asserting the existence of proofs of equality between two elements other than refl.

Are there any other reasonable implementations that would come with their own problems / tradeoffs?

In the above github discussion, Pierre-Marie Pédrot says that Lean's implementation of quotient types breaks subject reduction, then Mario Carneiro later arrives and says that this is a superficial problem with the quotient types rather than a fundamental one (it comes from the design choice that a quotient of a definitionally proof-irrelevant proposition is again definitionally proof-irrelevant; if one chose instead that quotients were proof-relevant types, this problem would not occur.)

Removing proof-irrelevance from the equation, is there a real risk of breaking subject reduction by adding quotient types?

The way it's currently implemented in the coq-HoTT library using private modules

private inductives not modules

Are there any problems that arise with this implementation? I guess it should break canonicity (?) because you're axiomatically asserting the existence of proofs of equality between two elements other than refl.

yes, and also private inductives are a hack which provide no guarantees in the kernel

ie if you have a plugin which implements eg something like `destruct`

and forgets to check that it's only run on non private inductives, the kernel won't complain

using ltac2 Constr.Unsafe probably works to ignore privacy too

Last updated: Feb 08 2023 at 23:03 UTC