3
$\begingroup$

Clarification of my terminologies:

  • Cubical canonicity: a generalized version of canonicity that the "generated by introduction rules" property holds in, not just closed context, but also contexts with only intervals.
  • Regularity: the fact that transport over a constant path reduces to the identity function.

Some work (\cite{CarloThesis}) has shown that regularity does not hold in general. However, cubical canonicity should imply that: in a closed context, any path is convertible to a constant path. Hence we can probably guarantee that closed paths are reflexive paths. So, do regularity hold in closed contexts? Can we assume closed regularity in compiled cubical code?

$\endgroup$
3
  • $\begingroup$ Can you make the statement of cubical canonicity more precise ? I thought that only homotopy canonicity (canonicity up to a path rather than definitional equality) could be proved for cubical type theories... $\endgroup$ Commented Jul 3, 2022 at 18:53
  • $\begingroup$ @kyodralliam basically as described in the abstract here: arxiv.org/abs/1607.04156 $\endgroup$
    – ice1000
    Commented Jul 5, 2022 at 15:04
  • 1
    $\begingroup$ Note that that result only explicitly states canonicity for $ℕ$. Usually I see experts state that regularity fails to hold for the universe, but holds in general for many types, e.g. $ℕ$. So, I thought an obvious example to try is something like $\mathsf{transport}\ \mathsf{refl}\ ℕ$. However, at least cubical Agda says this is judgmentally equal to $ℕ$, so this case of regularity holds as well. If it does fail for some closed term, I'm unsure how to write one (unless Agda is wrong here). $\endgroup$
    – Dan Doel
    Commented Jul 6, 2022 at 19:09

1 Answer 1

3
$\begingroup$

I'm a bit confused by:

However, cubical canonicity should imply that: in a closed context, any path is convertible to a constant path.

It's definitely not correct if the type in question is not hSet, or I misunderstand your claim. As far as I know, at least in CHM (and also in Cubical Agda), the operation hcomp is somewhat freely defined for general HITs. That means hcomp cannot be reduced whatever you put in its arguments. But it's still possible that any paths and even higher cubes in empty context are compositions of hcomp and the constructors. However, for ordinary inductive type, namely it does not involve any path constructors, your claim about canonicity is probably true, because basically you cannot define any paths other than refl and now hcomp can reduce. Try ℕ in Cubical Agda. But I'm not sure if anyone has done a proof.

I don't know much about other cubical theory. In CCHM, The operation transp (as a special case, transport) is defined inductively, as you may already know. For most type constructors, it reduces to transp in simpler types. For universe, it's just constant. For HITs, it is defined recursively for constructors. So if the construction of your type only involves these stuffs, regularity holds for it in the empty context. But it's incorrect for Glue type (and also for hcomp in universe) of which definition needs complicated correction of boundaries. No regularity should be expected in this case.

$\endgroup$
9
  • 1
    $\begingroup$ What is an example of a closed term that behaves irregularly, though? I even tried transp (λ j → notEq (i ∧ j)) (~ i) false to get a term of type (i : I) → notEq i. notEq i reduces to $\sf Glue$. Agda accepts the reflexive proof of: ∀ i → transport (λ k → notEq i) (b i) ≡ b i, so this example is regular, too, and it's not even closed with respect to the cubical context. Is this a bug? $\endgroup$
    – Dan Doel
    Commented Jul 19, 2022 at 17:37
  • $\begingroup$ I think hcomp in universe reduces to Glue (if you do have Glue) $\endgroup$
    – ice1000
    Commented Jul 19, 2022 at 17:44
  • $\begingroup$ @DanDoel The transp for Glue type results in a mixture of function application (by the corresponding equivalence) and hcomp (for boundary correction). So if you want irregular term, the boundary correction should really happen (it can be trivial in some cases) and hcomp for that type should not reduce, like a general HIT as I've mentioned. Type Bool is an ordinary inductive type. That's why it doesn't work. $\endgroup$ Commented Jul 20, 2022 at 0:34
  • $\begingroup$ @DanDoel As an example, consider a path defined by p i = Glue S¹ (λ { (i = i0) → (S¹ , idEquiv _) }), of which type is S¹ ≡ Glue S¹ empty. You will find transport (p ∙ sym p) base reduces to hcomp (λ i → empty) base and it isn't definitionally equal to base! $\endgroup$ Commented Jul 20, 2022 at 0:37
  • 1
    $\begingroup$ @ice1000 It's right in that paper. But in Cubical Agda, hcomp for universe is defined primitively and the rules are mimicking Glue. IIRC, it's called HCompU in its implementation. $\endgroup$ Commented Jul 20, 2022 at 0:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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