9
$\begingroup$

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!

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ 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) $\endgroup$
    – daniel gratzer
    Commented Mar 25, 2022 at 22:26
  • 3
    $\begingroup$ I think this question would be easier to read and answer if it included the partially working code verbatim. $\endgroup$
    – James Wood
    Commented Mar 25, 2022 at 22:35
  • $\begingroup$ I think stackoverflow.com/a/57653766/477476 and the followup stackoverflow.com/a/57800552/477476 contains useful info. Basically, you want to use that your codomain is Bool, which is an H-set. $\endgroup$
    – Cactus
    Commented Jun 4, 2022 at 14:17

1 Answer 1

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$

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.