Context: Cubical Type Theory
Consider a simple HIT, say, an
data HitInt : Set where pos : (n : ℕ) → HitInt neg : (n : ℕ) → HitInt posneg : pos 0 ≡ neg 0
Or, if you don't speak Agda we can use cubicaltt:
data int = pos (n : nat) | neg (n : nat) | zeroP <i> [ (i = 0) -> pos zero , (i = 1) -> neg zero ]
We want to define, for instance, a
succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:
sucHitInt : HitInt → HitInt sucHitInt (pos n) = pos (suc n) sucHitInt (neg zero) = pos 1 sucHitInt (neg (suc n)) = neg n sucHitInt (posneg x) = pos 1
Or in cubicaltt:
sucInt : int -> int = split pos n -> pos (suc n) neg n -> sucNat n where sucNat : nat -> int = split zero -> pos one suc n -> neg n zeroP @ i -> pos one
What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input Path".
My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path
pos 0 == neg 0 and returns
pos 1 -- say, matches a
Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a
<i> pos 1 (even this is not a member of the higher inductive family)?
What's interesting is that, in Agda it'll fill
pos 1 in the case body when I use Agda's proof-search.