I agree with the problem of using Glue types for the composition operation in the universe.
You could imagine an extra equation that Glue [ phi |-> (A, reflEquiv) ] A = A, but this is somehow unnatural.
However, it is what I was postulating in step 1 of the initial message of this thread.
You then need comp Box to respect Box^i [ phi |-> A ] A = A, and this is also apparently not possible in CCHM, but you now have the extra information that A is a line of types. (Using Box to turn an equivalence into a line of types in the definition of comp Box is circular.)
I've developed a notion of (regular) n-dimensional composition, which I think might suffice to complete the argument.
If you call a notion of Box that satisfies Box^i [ phi |-> A ] A = A "regular Box's", then the problem can be reduced to saying that to give regular 1-dimensional composition of regular 1-dimensional boxes, you need some sort of "(doubly) regular 2-dimensional composition" for A, and in CCHM such we can only get this "2-dimensional composition" which is regular in one direction or the other.
Of course (I haven't actually checked, but my intuition says that), once you have 2-dimensional composition you will need n-dimensional composition, and then hopefully regular (n+m)-dimensional composition for A will suffice to define regular n-dimensional composition of regular n-dimensional Box's.
Below I'll put an explanation of my idea of regular n-dimensional composition (returning an (n-1)-dimensional cube), since it feels unfair to say "I know how to do this" and hide "how to do this".
Unfortunately, it is quite complex; read at your own peril.
I don't yet know how to intelligibly describe n-dimensional composition for Glue and Box.
For now I'll just say that they should be essentially the same as in the 1-dimensional case, but with extra faces in the equiv and final hcomp steps corresponding to faces in the result.
In CCHM, the basic Kan operation is (comp^i A [ phi |-> a ] a0 : A(i1) [ phi |-> a(i1) ]) for i |- A with phi, i |- a : A and a0 : A(i0) [ phi |-> a(i0) ].
Regularity for this operation means that if A and a are independent of i, then comp^i A [ phi |-> a ] a0 = a0.
We have regular composition for Glue types, but we don't have comp^i (Glue [ phi |-> (A, equivRefl) ] A) = comp^i A.
Simplifying things a little, we can take hcom^i U [ phi |-> T ] A = Box^i [ phi |-> T(i := ~ i) ] A to be a new type former, and give that a regular composition operation.
Here the thing blocking us from getting comp^i (Box^j [ phi |-> A ] A) = comp^i A is that, given i, j |- T with phi, i, j |- t : T and t0 : T(i0)(j0)[ phi |-> t(i0)(j0) ],
we need a Path T(i1)(j1) (comp^i T(j1) [ phi |-> t(j1) ] (comp^j T(i0) [ phi |-> t(i0) ] t0)) (comp^j T(i1) [ phi |-> t(i1) ] (comp^i T(j0) [ phi |-> t(j0) ] t0)) which is refl if T is degenerate in i OR j.
This path plays the role that pres does in composition for Glue.
(I will write (i o j) for composition over j then over i, and (i = j) for composition over the diagonal (i = j). Then we want a path from (i o j) to (j o i) which is degenerate if T is degenerate in i OR j.
We can't construct such a doubly regular path, but we can postulate it as a new operation our types have to have, as a sort of regular composition over two dimensions simultaneously. Write (i ?'[a] j) for this, where a gives the location in the path.
However, my intuition tells me that while this two-dimensional regular composition may be preserved by all the usual type formers, optimistically including Glue and Box, because the two-dimensional composition for Box will have to satisfy an additional law comp2^i^j (Box [ phi |-> A ] A) = comp2^i^j A, we will end up needing some sort of three-dimensional analogue.
Once we need dimensions 1 and 2, we will almost certainly need dimension n.
But what should the type of three dimensional regular composition be? There are six ways to compose along the edges of a cube, forming a hexagon that we wan't to fill, but hexagons don't fit nicely into cubical type theory.
Here, we remember that there is one more way to compose across a square: along the diagonal (comp^k T(i,j:=k) [ phi |-> t(i,j:=k) ] t0), which agrees with composing either right then up or up then right when T is degenerate in i or j (with regularity).
Allowing diagonals, for each square we can give a path from the diagonal to going up then right, with swapping i and j giving a path to going right then up. Then if both of these are degenerate when T is degenerate in i or j, their composition is also, so we recover a path between (i o j) and (j o i). And this formulation can be extended to higher dimensions straightforwardly.
For each n-cube i_1, ..., i_n |- A, we have an n-dimensional regular composition operation which is a (n-1)-dimensional cube. Consider notation (i_1 ?[j_1] i_2 ?[j_2] ... ?[j_n-1] i_n) This is supposed to represent composition in an n-cube indexed by the i's, where our position in the resulting (n-1)-cube is given by the j's. We have to describe the faces of this cube, which we describe by saying that ?[0] reduces to = and ?[1] reduces to o.
Thus for 2-dimensional A, we have a line (i = j) --- (i ?[a] j) --- (i o j), and for three dimensional A, we have a square with four faces (i = j ?[a_2] k), (i o j ?[a_2] k), (i ?[a1] j = k) (i ?[a1] j o k), relating the four corners given by coercing over i then j then k, coercing over i then j and k simultaneously, coercing over i and j simultaneously then coercing over k, and coercing over i, j, and k simultaneously.
The point is that this gives a well-defined notion of cube.
We also have to define the regularity condition: what happens when A, a are degenerate in i_k? We require that (i_1 ... i_k-1 ?[j_k-1] i_k ?[j_k] i_k+1 ... i_n) is equal to (i_1 ... i_k-1 ?[j_k-1 v j_k] i_k+1 ... i_n), treating j_0 = j_n = 1.
Extending this to = and o, if A, a are degenerate in i, then (i = j) and (i o j) reduce to (j).
On a two-dimensional cube, this says that (i ?[a] j) reduces to (j) when A, a are degenerate in i, and to (i) when A, a are degenerate in j.
(That this is all coherent is obvious to me, but I have no idea how to explain it well)
This all gives a notion of n-dimensional regular composition, which takes an n-cube type A and partial term phi, i1, ..., in |- a and a base point a0 : A(i_k := 0)[ phi |-> a(i_k := 0) ] and returns an (n-1)-cube in A(i_k := 1) [ phi |-> everywhere a(i_k := 1) ].
There are three classes of equations that this has to satisfy, two for the face maps j_k = 0 and j_k = 1 in the output, and one for when A, a are degenerate in i_k.
In the one-dimensional case, this is the same as the specification of the usual regular comp.
Considering j_k to be formally extended with j_0 = j_n = 1, we get a "zero-dimensional" composition operation, which should be taken to be the identity. (I have no idea what it would mean to let j_0 and j_n vary)
I am reasonably confident that this operation is closed under usual type formers (Pi, Sg, Path, ...) by essentially the same argument as for 1-dimensional comp.
I think I have worked out how to give a regular n-dimensional composition operation for Glue, by essentially the same argument as in CCHM, but with additional faces for j_k = 1 in the equiv and final hcomp steps.
In this setting, we want Box to also be m-dimensional: j_1 ... j_n-1 |- Box^i1...^im _{j_1}..._{j_n-1} [ phi |-> T ] A for phi, i1, ..., im |- T, with phi |- A = T(i_k := 1).
I think I have worked out how to give a regular n-dimensional composition operation for m-dimensional Box, using essentially the same argument as for Glue, but replacing pres with the composition of two paths given by (m+n)-dimensional regular composition.
To use Box as the regular n-dimensional composition operation for the universe, we need that (Box, comp Box) respects the equations for when j_k = 0, j_k = 1, or T is independent of j.
My hope is that, as in the (1, 1) dimensional case, using (m+n)-dimensional regular composition for pres will make this work.
I have sketched on paper that composition for Glue and Box are regular, but that is already pushing the limits of my confidence in paper calculations.
Checking that comp Box respects the equations that it needs to is another layer more complex, and I haven't managed to do so on paper.
However, by analogy with the (1, 1) dimensional case, I am hopeful.