How do I handle the higher inductive cases when defining functions on HITs?

Question

I'm experimenting with Homotopy Type Theory in Agda. I use HITs to define the integers:

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Data.Nat using (ℕ; _+_)

data ℤ : Set where
  -- | An integer i is a pair of natural numbers (m, n)
  --   where i = m - n
  int : ℕ → ℕ → ℤ
  -- | (a, b) = (c, d)
  --   a - b = c - d
  --   a + d = b + c
  int-eq : ∀ {a b c d : ℕ} → (a + d ≡ b + c) → int a b ≡ int c d

Now, I want to define addition on the integers:

add-ints : ℤ → ℤ → ℤ
add-ints (int a b) (int c d) = int (a + c) (b + d)

However, the compiler gives an error because I need to pattern match the equality constructors as well:

Incomplete pattern matching for add-ints. Missing cases:
  add-ints (int-eq x i) (int x₁ x₂)
  add-ints x (int-eq x₁ i)
when checking the definition of add-ints

So, I end up with this:

add-ints : ℤ → ℤ → ℤ
add-ints (int a b) (int c d) = int (a + c) (b + d)
add-ints (int-eq x i) (int c d) = { }0
add-ints (int a b) (int-eq x i) = { }1
add-ints (int-eq x i) (int-eq y j) = { }2

Agda's typed holes don't help:

?0 : ℤ
?1 : ℤ
?2 : ℤ

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  ?0 (x = x) (i = i) (c = a) (d = b)
    = ?2 (x = x) (i = i) (y = x₁) (j = i0)
    : ℤ
  ?0 (x = x) (i = i) (c = c) (d = d)
    = ?2 (x = x) (i = i) (y = x₁) (j = i1)
    : ℤ
  ?1 (a = a₁) (b = b₁) (x = x₁) (i = i)
    = ?2 (x = x) (i = i0) (y = x₁) (j = i)
    : ℤ
  ?1 (a = c₁) (b = d₁) (x = x₁) (i = i)
    = ?2 (x = x) (i = i1) (y = x₁) (j = i)
    : ℤ
  int (a + x) (b + x₁) = ?0 (x = x₂) (i = i0) (c = x) (d = x₁) : ℤ
  int (c + x) (d + x₁) = ?0 (x = x₂) (i = i1) (c = x) (d = x₁) : ℤ
  int (x + a) (x₁ + b) = ?1 (a = x) (b = x₁) (x = x₂) (i = i0) : ℤ
  int (x + c) (x₁ + d) = ?1 (a = x) (b = x₁) (x = x₂) (i = i1) : ℤ

The Agda documentation gives examples of HIT usage, where it pattern matches on the equality constructors when operating on the torus and propositional truncation. However, as someone without a background in topology, I don't completely follow what's going on.

What is the purpose of the i and j from the [0, 1] interval, and why do they appear in my equality constructor patterns? How do I use i and j? How do I handle the higher inductive cases?

Calamint

Very related question, also I ended up doing a talk from the "indurstry programmer manages to add two integers" angle, slides are here both are about adding Ints in your HIT representation in Cubical Agda. – Latria

@Latria Thank you for finding that question. Now, I see that I need to add another higher inductive constructor to make the equalities equal. With the question that you link, my entire question has been answered. – Calamint

Answer 1

You can think of path constructors as taking an interval variable, and satisfying additional equations about the endpoints of that interval,

data ℤ : Set where
  int : ℕ → ℕ → ℤ
  int-eq : ∀ {a b c d : ℕ} → (a + d ≡ b + c) → I → ℤ
   -- such that int-eq {a} {b} {c} {d} _ i0 = int a b
   -- and       int-eq {a} {b} {c} {d} _ i1 = int c d

In your equations for add-ints of int-eq you also have to produce a ℤ, and it has to match the first clause (for the int constructor) at both endpoints. These are the constraints that Agda reports, saying that the different clauses have to agree.

You can start with ?0 first. For which only the last two contraints matter. It helps here to fill in the implicit variables,

add-ints (int-eq {a0} {b0} {a1} {b1} x i) (int c d) = { }0

To match the first clause, you need to come up with a value of type ℤ that is equal to int (a0 + c) (b0 + d) when i = i0 and equal to int (a1 + c) (b1 + d) when i = i1. You can use an int-eq constructor for this,

?0 = int-eq {a0 + c} {b0 + d} {a1 + c} {b1 + d} ?4 i

The equality ?4 has to be worked out.

Discourtesy

Thank you. Because of your help, I was able to prove the cases where I matched on int-eq and int. However, I've been working on the case where I match on two int-eqs, and I'm stumped. In my partial proof, I have two integer sums that I created via int-eq and i, and I need to prove that they are equal relative to j. I informally proved it by proving each "end" of the equality individually, but I can't pattern match on i and j, so I can't refine the cases. The documentation shows that you can match on interval inhabitants by using "Partial," but I don't understand it. Am I on the – Calamint

right track with the pattern matching, or is there another way to do this? – Calamint

If you have both an i and a j in scope then you are supposed to provide a 2-dimensional square, and it's not enough to do it for the "ends", it has to provide the middle parts too. In some cases hcomp can help, but here it might just be that you want to add a constructor of type isSet ℤ, so that you know squares can always be filled. – Diglot

I would gladly up-vote this answer if it were giving the full solution. – Prae

@Diglot Could you please elaborate both solutions (hcomp and isSet ℤ)? – Prae

Spoiler alert: here is a full solution for the set-truncated case. – Latria