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?

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. — Cactus
@Cactus 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. — Del

Twan van Laarhoven Twan van Laarhoven · Accepted Answer · 2019-09-10T11:49:58

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.

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

1 Answers