{-# OPTIONS --cubical --safe #-}
module 2019-4-21-CuttMltt where
import Agda.Builtin.Equality as MLTT
import Cubical.Core.Everything as CUTT
import Agda.Builtin.Nat as MNat
import Cubical.Data.Nat as CNat
private variable A B : Set

In dependently-typed programming languages, we do equality proofs. Type Theory folks formed two groups; one stands for “proofs are not important”, one stands for “proofs are important”. Someone claims that the identity proof between two objects is unique – which is related to the K rule. The other people believe that the proof of identity is significant – the same theorem can have different proofs, where the identity relation on these proofs are also nontrivial and can be proved to be equivalent or not.

Intuitionistic Logic

First, let’s take a look at the world of unique identity proofs.

module Intuitionistic where
 open MLTT
 open MNat

In Intuitionistic Logic, we can prove new theorems via pattern matching on existing theorems, because identity proofs are instances of the equality type:

 trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
 trans refl refl = refl
 sym : {a b : A} → a ≡ b → b ≡ a
 sym refl = refl
 cong : {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
 cong _ refl = refl

or we can use rewrite, which is syntactic sugar of pattern matching (and this definition is more Idris style):

 trans₁ : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
 trans₁ p q rewrite p = q
 cong₁ : {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
 cong₁ _ p rewrite p = refl

These three functions, trans, sym and cong are our equality proof combinators. Larger and more concrete theorems, such as the plus commutative law:

 +-comm : ∀ a b → a + b ≡ b + a

can be proved by induction – the base case is simply a ≡ a + 0, where we can introduce a lemma for it:

 +-comm zero b = +-zero b

… and we prove the lemma by induction as well:

  where
  +-zero : ∀ a → a ≡ a + 
  +-zero zero = refl
  +-zero (suc a) = cong suc (+-zero a)

Very small theorems can be proved by induction trivially using a recursive call as the induction hypothesis and let the cong function to finish the induction step. Combining induction and our trans combinator we get the induction step of the proof of the plus commutative law:

 +-comm (suc a) b = trans (cong suc (+-comm a b)) (+-suc b a)
  where
  +-suc : ∀ a b → suc (a + b) ≡ a + suc b
  +-suc zero _ = refl
  +-suc (suc a) b = cong suc (+-suc a b)

On the other hand, even large theorems such as the plus commutative law can also be proved without the help of lemmas. Here’s an example, by exploiting the rewrite functionality:

 +-comm₁ : ∀ n m → n + m ≡ m + n
 +-comm₁ zero zero = refl
 +-comm₁ zero (suc m) rewrite sym (+-comm₁ zero m)  = refl
 +-comm₁ (suc n) zero rewrite +-comm₁ n zero = refl
 +-comm₁ (suc n) (suc m) rewrite +-comm₁ n (suc m)
  | sym (+-comm₁ (suc n) m) | +-comm₁ n m = refl

What does rewrite do? Let’s look at it in detail. To prove this theorem, whose goal is a + c ≡ b + d,

 step-by-step : ∀ {a b c d} → a ≡ b → c ≡ d → a + c ≡ b + d
 step-by-step {b = b} {d = d} p q

we first rewrite with p, which turns the goal to b + c ≡ b + d, then rewrite with q, which turns the goal to b + d ≡ b + d,

  rewrite p | q

which is a specialized version of refl:

  = refl {x = b + d}

It’s like we’re destructing our goal step by step and finally turn it into a specialized refl. For more complicated proofs, we’re not only destructing the goal – we’re also constructing terms that can be used to destruct the goal. rewrite is how we use the constructed terms to destruct terms. Our proof is bidirectional.

Cubical model

What if the identity proofs are not trivial?

module Cubical where
 open CUTT using (_≡_; I; ~_; hcomp; inS; hfill; i0; i1)
 open CNat

In the Cubical model, there’s no pattern matching because you can never tell how many proofs there can be (so no case analysis). Instead, there are interval operations that can construct proofs via existing proofs in a more detailed way. Inverting an interval is sym:

 sym : {a b : A} → a ≡ b → b ≡ a
 sym p i = p (~ i)

Creating a new interval by combining an old path with an arbitrary function is cong:

 cong : {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
 cong f p i = f (p i)

trans is far more complicated – you’ll need cubical kan operation:

 trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
 trans p q i = hfill (λ { j (i = i0) → p i; j (i = i1) → q j}) (inS (p i)) i

Although we lose the ability to rewrite, we still have our combinators – sym, cong and trans, which means that several existing proofs are still perfectly valid under the Cubical model. On the other hand, according to the design of Path types, some proofs become perfectly natural. For instance, the step-by-step theorem shown above can be proved by:

 step-by-step : ∀ {a b c d} → a ≡ b → c ≡ d → a + c ≡ b + d
 step-by-step p q i = p i + q i

There can also be equality on functions, which is not even possible in the Intuitionistic type theory:

 funExt : {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
 funExt p i a = p a i

Obvious Conclusions

• The Cubical model introduces tons of primitives while it’s fairly more powerful than the Intuitionistic type theory
• Cubical model is harder implementation-wise
• Intuitionistic type theory is more friendly for letting the compiler to solve some unification problems
• Both of these two models are not gonna save Agda