Subtypes in Cubical Type Theory I have yet another question about CuTT.
In the CCHM paper, a notion of cubical subtypes is introduced. A term of a subtype is generally written $\Gamma \vdash x : A[\phi \Rightarrow u]$ and is a shorthand for $\Gamma \vdash x : A \quad \Gamma, \phi \vdash x \equiv u : A$.
I understand the role of this notion in the circumstances it was introduced (as CCHM basically describes the operations of a cubical typechecker).
However, this notion is present for example in the Cubical Agda, and I don't see why. Is it actually useful for typechecking in some circumstances?
I know that all composition and glue types use the subtypes in Agda, but I think that's because of the way how the cubical primitives are defined. Since they're defined by subtypes, all derived notions must use subtypes. But wouldn't additional internal reduction rules for eg. unglue terms suffice?
 A: This is rather on the edge of my knowledge of the subject, but I think the answer is something like this:
Cubical Agda has a bunch of very primitive functions for some of the cubical operations whose types do not completely describe the rules for using them. For instance, we have something like:
hcomp : (∀ i → Partial φ A) → A → A

This looks like you can just provide a partially specified A and another A, and get a resulting A, which is supposed to agree with the partial value on φ. But, when you try to use it, Agda will check that the second A actually agrees with the partial definitions under certain conditions, and reject your code if this doesn't happen.
Now, this isn't a problem when  you're directly using hcomp with some definitions you wrote that are definitionally equal in the expected ways. But this makes hcomp not a first class construction. It is a primitive operation with side conditions on its use, and if you try to write something like:
myhcomp : (∀ i → Partial φ A) → A → A
myhcomp u x = hcomp u x

Agda will reject your program, because the arbitrary values your function takes do not necessarily satisfy the definitional equalities required for hcomp to be valid. And this is where the subtypes come in, because they are how you abstract over values with the necessary definitional equalities. You can actually write:
myhcomp : ∀{φ} → (u : ∀ i → Partial φ A) → Sub A φ (u i0) → A
myhcomp u x = hcomp u (outS x)

because outS x satisfies the correct definitional equalities with respect to u i0. Sub A φ (u i0) is basically the type of x values with this property, and there is no other mechanism for abstracting over definitional equalities like this, I think (I guess Path(P) also does, but in general you'd have to fill in the components above to get values of those types).
If you aren't using some of the wrappers around hcomp, like the full type changing comp, then you might not notice this being useful, because you are just writing things where the reduction of terms satisfies the side conditions. But I think comp wouldn't even be possible to write without Sub, and it wouldn't be possible to write these sort of abstractions on top of the primitive operations.
