I am a simple man who does not really understand all the ins and outs of Cubical Agda. I have attempted to read its docs, and HoTT, and stopped following what was going on fairly quickly.
What I am specifically hoping for is an example of how to write a simple operation for a higher inductive type, ideally without libraries outside of Cubical.Core.Everything.
For a specific example, let's consider the integers as a quotient over pairs of naturals:
data N : Set where
0N : N
suc : N -> N
_+N_ : N -> N -> N
0N +N n = n
suc m +N n = suc (m +N n)
data Z : Set where
zpair : N -> N -> N
zeq : (a b c d : N) -> (a +N d) === (b +N c) -> zpair a b === zpair c d
_+Z_ : Z -> Z -> Z
zpair a b + zpair c d = zpair (a +N c) (b +N d)
zeq a b c d ad=bc i + zeq e f g h eh=fg j = ???
I can and have worked my way through e.g. zpair + zeq and vice versa, where there's an i : I and I can just construct an appropriate path and apply it to i. I don't understand what to do when I have i j : I and I'm combining the points on the paths together, and in particular it doesn't look like I can just wedge them together, nor do I see an obvious composition or a value in I to apply it to.
A satisfactory answer would fill in the ???, assuming any necessary convenient lemmas on _+N_ and using the equational reasoning API as necessary.
I've looked at definitions of the integers in Agda that define them as a quotient, but I can't find where this sort of operation is defined.
The usual approach to this is to add a set truncation constructor, like
squash : isSet Z
This ensures that you can fill in any square in Z, for example using isSet→SquareP. (Note that isSet Z unfolds to something that has the right shape to be used as the type of a higher constructor.)
You can see this approach in action in the cubical library here: note that ℤ is defined as the quotient of ℕ × ℕ by some relation rel, where quotients are defined as a higher inductive type with a squash/ constructor that forces the quotient to be a set.
For another approach that does not require truncating, see the 1lab: here we restrict the path constructor to relating pairs of the form (x, y) and (x + 1, y + 1). You can convince yourself that this does not introduce any non-trivial loops, so that the resulting HIT is a set (start by drawing ℕ × ℕ as a grid, then draw a line between every pair of points that is related by a path; do you see how this differs from the previous approach?).
Once this is in place, it is common to abstract away the details of the implementation by defining a recursion principle for the integers, which often can have a simpler form if we assume that the target type is of lower h-level (in this case, a set).