# Case splitting with quotient types in Cubical Agda

I'm getting started with Cubcal Agda and I'm quite confused.

I've got a HIT A defined, with a path constructor eq returning a ≡ b and a squash path constructor ∀ {x y : A} → (p1 p2 : x ≡ y) → p1 ≡ p2. Basically it's a quotient type.

I've got a function f: A -> Bool, and in the case for squash {x} {y} p1 p2 i j I get boundary conditions that look like this?

i = i0 ⊢ f (p1 j)
i = i1 ⊢ f (p2 j)
j = i0 ⊢ f x
j = i1 ⊢ f y


Frankly, I have no idea what this means.

I intuitively get that for eq i, I need to show that f a ≡ f b. What I'm actually doing providing an expression parameterized over i, that evaluates to f a for i0 and f b for i1. But when it comes to the higher case with squash I'm lost.

Is there a good intuition for what I'm actually trying to show in the squash case? Is there any way to handle the cases for path constructors by directly providing equalities, rather than values with boundary conditions?

Or is having the squash case a mistake? I added it because I'm trying to show (x : A) -> Dec (x ≡ a), and in the case for eq I end up having to show equalities between equalities. I thought adding squashwould help with that, but maybe I'm wrong?

Thanks for the help!

• If it helps, you can read this as asking you to provide a homotopy between $p_1$ and $p_2$. This is the direct equivalent of the case for your path constructor, as you're now in the position of providing paths between two paths. The first two boundaries express that it's a square between the two supplied paths and the last two ensure this square is constant on the extremes (a homotopy of paths). This should be be possible to handle easily using the fact that boolean are a set. (Apologies for any typos, written on mobile) Mar 25 at 22:26
• I think this question would be easier to read and answer if it included the partially working code verbatim. Mar 25 at 22:35

It means that your implementation of the squash case, let's call it u (where u may refer to i, j, p1, p2, etc., and can perform recursion), must satisfy the following definitional equalities:

• u [i ↦ i0] = f (p1 j)
• u [j ↦ i0] = f x
• Other two omitted, you can easily find the pattern

Without using Glue, it will be very difficult to fill the two goals in a nontrivial way. You HIT is essentially the unit type, so it's quite boring. I suggest starting with something interesting, like the circle/interval/etc., to get the basic intuition, because you actually get some paths to preserve.