# Inductive Types with Path Constructors

## ⇦ Previous · Index · Next ⇨

Recall the previous post, in which we had higher dimensional paths (squares) and we can use path application to reduce their dimensions.

{-# OPTIONS --cubical --allow-unsolved-metas #-}
module HITs where
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Agda.Builtin.Nat
variable A : Set
6.2s
Agda

Recall our classical integer definition (click the Int to see):

import Cubical.Data.Int using (Int)
25.9s
Agda

It's (kind of) bad as it's not symmetric -- Taking the number two as an example, positive two is pos 2, while negative two is negsuc 1. Proving the associative law on the addition operation of this integer is a pain in the ass due to the lack of symmetry (take a glance at here) on this integer (the definition is not symmetric, therefore the operations are naturally not symmetric as well).

We may want a symmetric version of integers -- imagine something like this:

data Int : Set where
  pos : Nat -> Int
  neg : Nat -> Int
0.7s
Agda

but now we're having two zeros -- pos 0 and neg 0. We define the classical integer not symmetrically intentionally to avoid the presence of two zeros, as mathematically we claim that zero is neither positive nor negative (we can say it in another way that there's positive zero but not negative).

Question: can we tell Agda that pos 0 is equal to neg 0? If so, the above definition will be usable!

The answers is yes yes yes, YES!

## Path Constructor

Recall that paths are:

1. Defined as functions whose domains are intervals and codomains are the endpoints' types

2. Treated as an equivalence relation

we can add constructors that are paths, to a datatype, like adding pos 0 ≡ neg 0, which is a path (and if there's a definition of such path, it's gonna be a function from interval to Int), to Int:

  zro : pos 0 ≡ neg 0
0.8s
Agda

If we rewrite the type of zro using a function type (while zro itself has a path type) we get a constructor-ish type (whose return type is the type it's constructing):

zroFn : I -> Int
zroFn i = zro i
0.8s
Agda

Since zro returns an Int and it's a constructor, we call it "path constructor". Before introducing some advanced properties of path constructors, we can already have a lot of fun stuffs like this:

posneg : pos 0 ≡ neg 0
posneg = zro
negpos : neg 0 ≡ pos 0
negpos i = zro (~ i)
0.7s
Agda

## Path Constraints

What's special about path constructors is that they also constraint your pattern matching clauses when a datatype with path constructors appear at the left-hand-side of the pattern matching clauses. I'll go with an example -- the succ function. When we write the succ function for Int, we'll need to pattern match over the path constructor:

succ : Int -> Int
succ (pos x) = pos (suc x)
succ (neg zero) = pos 1
succ (neg (suc x)) = neg x
-- The above three clauses are trivial
succ (zro i) = -- What should we return in this case?
Agda

Well, the rule for the path constructor case is that, we can return anything satisfying (taken this succ on Int for instance):

• succ (zro i) should reduce (definitionally equal) to:

• succ (pos 0) (the pos 0 comes from zro i0) when i equals (substituted with) i0

• succ (neg 0) (the neg 0 comes from zro i1) when i equals (substituted with) i1

We may call this property for short "the path endpoints are respected".

and because both succ (pos 0) and succ (neg 0) equals to pos 1, the only possible body for the zro case will be pos 1.

succ : Int -> Int
succ (pos x) = pos (suc x)
succ (neg zero) = pos 1
succ (neg (suc x)) = neg x
succ (zro i) = pos 1
0.8s
Agda

In fact, Agda's constraint solver is abled to solve some clauses of the function. We can write the above function with holes:

succ′ : Int -> Int
succ′ (pos x) = pos (suc x)
succ′ (neg zero) = {!!}
succ′ (neg (suc x)) = neg x
succ′ (zro i) = {!!}
0.7s
Agda

Due to the presence of the path constructor whose type is pos 0 ≡ neg 0, Agda knows succ' (neg zero) is equal to succ' (pos zero), where succ' (pos x) is defined as pos (suc x), applying the pattern with pos zero results in pos (suc zero), which is pos 1.

Similarly, we can define the pred function:

pred : Int -> Int
pred (pos zero) = neg 1
pred (pos (suc x)) = pos x
pred (neg x) = neg (suc x)
pred (zro i) = neg 1
0.8s
Agda

## Isomorphism

module IsoInt where
 open Cubical.Data.Int renaming (Int to StdInt)
 pattern spos n = StdInt.pos n
 pattern nsuc n = StdInt.negsuc n
0.8s
Agda

Given the standard Integer definition, we can prove that the HIT (short for higher-inductive types, that are inductive types with path constructors) integer is isomorphic to it. To prove isomorphism under type theory, we need to provide two function that (in fact, only known to us) are inverse to each other, and prove this inverse relation (to convince Agda that they are inverse).

From StdInt to Int, we turn pos into pos, and negsuc into neg ∘ suc:

 StdInt->Int : StdInt -> Int
 StdInt->Int (spos n) = pos n
 StdInt->Int (nsuc n) = neg (suc n)
0.8s
Agda

On the other hand, due to the absence of path constructors in the standard definition, we map zro i to pos 0.

 Int->StdInt : Int -> StdInt
 Int->StdInt (pos x) = spos x
 Int->StdInt (neg zero) = spos 0
 Int->StdInt (neg (suc x)) = nsuc x
 Int->StdInt (zro i) = spos 0
0.7s
Agda

Let's try to prove the two functions are actually inverse to each other. One side of the isomorphism is trivial:

 StdInt->Int->StdInt : (n : StdInt) -> Int->StdInt (StdInt->Int n) ≡ n
 StdInt->Int->StdInt (spos _) = refl
 StdInt->Int->StdInt (nsuc _) = refl
0.7s
Agda

This is provable because our two patterns substitutes Int->StdInt (StdInt->Int n) into Int->StdInt (StdInt->Int (spos n)) and Int->StdInt (StdInt->Int (nsuc n)), which unfolds to spos n and nsuc n, identical to the right-hand-side of the path in the return type.

Two cases of the other side of the isomorphism is a bit harder, I'll talk about'em one by one (Agda cell will follow below).

 Int->StdInt->Int : (n : Int) -> StdInt->Int (Int->StdInt n) ≡ n
 Int->StdInt->Int (pos x) = refl
 Int->StdInt->Int (neg zero) =
Agda

This clause is the first non-trivial case. If we substitute Int->StdInt n with neg zero, we get spos 0, while substituting StdInt->Int n with spos 0 we get pos 0. Therefore this clause has type pos 0 ≡ neg 0, which is exactly the type of zro.

  zro
Agda

Then we fill another trivial case.

 Int->StdInt->Int (neg (suc x)) = refl
 Int->StdInt->Int (zro i) = lemma
  where
Agda

The last case is also a bit complicated, we're introducing a lemma here for readability. Doing some simple substitution we can come up with the following signature:

  lemma : pos 0 ≡ zro i
  lemma j =
Agda

This is a path with an interval variable in the context, which can be seen as a path between paths. The two sides of the paths are pos 0 and zro i, while pos 0 (the j = i0 side -- I mean the x = y (x is an interval variable, y is i0 or i1) side by the y endpoint of the path indexed by x) is a constant value but zro i (the j = i1 side) has two different sides pos 0 (the i = i0 side) and neg 0 (the i = i1 side).

To solve a cubical problem, we observe it by graphing it:

This is exactly the minSq introduced in the previous blog post (substituting a with pos 0, b with neg 0)! Recall that the minSq is defined with the min operator, we apply the same technique here:

    zro (i ∧ j)
Agda

We're done!

 Int->StdInt->Int : (n : Int) → StdInt->Int (Int->StdInt n) ≡ n
 Int->StdInt->Int (pos x) = refl
 Int->StdInt->Int (neg zero) = zro
 Int->StdInt->Int (neg (suc x)) = refl
 Int->StdInt->Int (zro i) = lemma
  where
   lemma : pos 0 ≡ zro i
   lemma j = zro (i ∧ j)
1.2s
Agda

### Isomorphism and Path

A nice thing that the Cubical Type Theory can bring you is that you can create a path between isomorphic types. The theory behind is beyong the topic of this blog, but we can have a try on the library function based on the theory:

 Int≡StdInt : Int ≡ StdInt
 Int≡StdInt = isoToPath (iso Int->StdInt
                             StdInt->Int
                             StdInt->Int->StdInt
                             Int->StdInt->Int)
0.7s
Agda

## A problem

There's another integer type defined as HIT:

infixl 5 _⊝_
data DeltaInt : Set where
  _⊝_    : Nat -> Nat -> DeltaInt
  cancel : ∀ a b -> a ⊝ b ≡ suc a ⊝ suc b
0.7s
Agda

It's defined as one natural substracted by another. This is a brand new HIT, so I recommend readers to define some common operations for it and prove their properties to get familiar with this HIT.

We can imagine a lemma of which like this:

cancelDiamond : ∀ a b i → cancel a b i ≡ cancel (suc a) (suc b) i
cancelDiamond a b = {!!}
0.9s
Agda

Since a ⊝ b is equal to suc a ⊝ suc b, we can generalize this equality relation over an interval (which is exactly the cancelDiamond function). But how do we prove this? Try graphing cancelDiamond, we see a square, but it's neither a min nor a max square.

The answer will be revealed in the next blog post using new cubical operations.