In this formulation of quotient types in cubical type theory I was able to implement an eliminator and use that to implement basically curried function application. However, in all this, the only requirement on the factoring relation is that it is reflexive.

I find this surprising. I would have expected transitivity and symmetry to also be needed somewhere along the way. Is there an intuitive explanation for why reflexivity is enough?


Your Quot construction is a set-truncated quotient by an arbitrary relation $R$ since you never use the reflexivity assumption in the construction. That is, you don't even need the reflexivity of $R$ to perform the quotient and derive its basic properties.

As the HoTT book explains in Section 6.10, it is perfectly possible to make set-truncated quotients by an arbitrary relation because reflexivity, transitivity and symmetry are taken care of by the paths themselves (because there are identity paths, paths can be reversed, and composed). That is, the quotient $A/R$ is equivalent to the quotient $A/\overline{R}$ where $\overline{R}$ is the equivalence relation generated by $R$.

There is one property that you will not get, namely that (using the notations from your file) $(x : A) \to (y : A) \to \mathsf{point}\;x = \mathsf{point}\;y \to R\;x\;y$. For that you need the fact that $R$ is a proposition and an equivalence relation.

  • $\begingroup$ No wait, I actually am using the reflexivity of the underlying relation, namely, when I am turning a pair of quot {x} {y} eq i and a point a into a quot (eq , (? : a ≈ a)) i. $\endgroup$ – Cactus Nov 13 '18 at 12:49
  • $\begingroup$ Hmm, can't do this right now, the HoTT book Section 6.10 should state an appropriate elimination principle, please compare that with the one you've stated. $\endgroup$ – Andrej Bauer Nov 13 '18 at 13:00
  • $\begingroup$ For representation-invariance, in my eliminator I ask for ∀ {x y} (eq : x ∼ y)→ PathP (λ i → P (quot {x = x} {y = y} eq i)) (point* x) (point* y)), I can't imagine what else I would possibly require. $\endgroup$ – Cactus Nov 13 '18 at 13:05
  • $\begingroup$ Here is the HoTT-Agda formulation of set-quotients. I don't know enough of Agda do decipher what you're doing (what is PathP, I see it's something cubical, but what?), I hope that helps. $\endgroup$ – Andrej Bauer Nov 13 '18 at 16:50
  • 1
    $\begingroup$ Yes, I see. You're defining there a map $A_1/R_1 \to A_2/R_2 \to (A_1 \times A_2)/(R_1 \times R_2)$. That in itself has nothing to do with the definition of quotients., but rahter with the interaction between quotients and products. I think it's a bit more sophisticated than what you did. Let me think. $\endgroup$ – Andrej Bauer Nov 14 '18 at 14:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.