Mfrhtyj

Context: Cubical Type Theory

Consider a simple HIT, say, an HitInt:

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 Path like <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.

it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer

My understanding is that it matches points of path rather than path itself. This is why the matching is on posneg x (where x : I) rather than posneg itself.

Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a special of regular constructors, i.e.

  posneg : I ↝ HitInt [i0 ↦ pos 0 ; i1 ↦ neg 0]

where if you ignore "special" properties of Interval, it looks like a regular constructor (in cubicaltt notation it already looks similar except that I is always treated specially).

What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.

It's the only way to satisfy constraints imposed by previous definitions (this works for both zero cases). In fact, Agda can correctly solve even two holes (in right order):

sucHitInt : HitInt → HitInt

sucHitInt (pos n) = pos (suc n)

sucHitInt (posneg i) = {!!}

sucHitInt (neg zero) = {!!}

sucHitInt (neg (suc n)) = neg n

Why it's not returning a Path like pos 1 (even this is not a member of the higher inductive family)?

Again, since we're matching on points rather than paths; for symmetry it's possible to imagine that case as equal to:

sucHitInt (posneg i) = (λ _ → pos 1) i

reading somewhat like "for all projections from I at i to path posneg we have projections from I at I to constant path (λ _ → pos 1)". This doesn't quite work in Agda (because typecheking lambda application directly isn't very well supported), however the following (with the same meaning) does:

sucHitInt (posneg i) = refl {x = pos 1} i

Finally, abusing notation, we could rewrite that as

(ap sucHitInt posneg) i = (refl {x = pos 1}) i

(where ap (from the HoTT book) corresponds to cong in typical Agda) and, getting rid of i from the both sides, recover path to path mapping.

PS: i'm new to cubical myself, so hopefully someone can correct or extend my answer