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?

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.