From 3d2a6a08a439afb9da65fe48679889d211ed9a05 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 6 Aug 2015 17:52:49 +0200
Subject: [PATCH] feat(hott/nat): add characterization of equality in nat

---
 hott/book.md              |  4 ++--
 hott/types/nat/hott.hlean | 38 ++++++++++++++++++++++++++++++++++----
 2 files changed, 36 insertions(+), 6 deletions(-)

diff --git a/hott/book.md b/hott/book.md
index 6395800f0..1bafddc21 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -16,7 +16,7 @@ The rows indicate the chapters, the columns the sections.
 |       | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 |
 |-------|---|---|---|---|---|---|---|---|---|----|----|----|----|----|----|
 | Ch 1  | . | . | . | . | + | + | + | + | + | .  | +  | +  |    |    |    |
-| Ch 2  | + | + | + | + | . | + | + | + | + | +  | +  | -  | -  | +  | +  |
+| Ch 2  | + | + | + | + | . | + | + | + | + | +  | +  | -  | +  | +  | +  |
 | Ch 3  | + | - | + | + | ½ | + | + | - | ½ | .  | +  |    |    |    |    |
 | Ch 4  | - | + | - | + | . | + | - | - | + |    |    |    |    |    |    |
 | Ch 5  | - | . | - | - | - | . | . | ½ |   |    |    |    |    |    |    |
@@ -62,7 +62,7 @@ Chapter 2: Homotopy type theory
 - 2.10 (Universes and the univalence axiom): [init.ua](init/ua.hlean)
 - 2.11 (Identity type): [init.equiv](init/equiv.hlean) (ap is equivalence), [types.eq](types/eq.hlean) and [types.cubical.square](types/cubical/square.hlean) (characterization of pathovers in equality types)
 - 2.12 (Coproducts): not formalized
-- 2.13 (Natural numbers): not formalized
+- 2.13 (Natural numbers): [types.nat.hott](types/nat/hott.hlean)
 - 2.14 (Example: equality of structures): algebra formalized in [algebra.group](algebra/group.hlean).
 - 2.15 (Universal properties): in the corresponding file in the [types](types/types.md) folder.
 
diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean
index 81fd91027..b7e1e3bad 100644
--- a/hott/types/nat/hott.hlean
+++ b/hott/types/nat/hott.hlean
@@ -30,10 +30,6 @@ namespace nat
   definition le_succ_equiv_pred_le (n m : ℕ) : (n ≤ succ m) ≃ (pred n ≤ m) :=
   equiv_of_is_hprop pred_le_pred le_succ_of_pred_le
 
-  set_option pp.beta false
-  set_option pp.implicit true
-  set_option pp.coercions true
-
   theorem lt_by_cases_lt {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
     (H3 : a > b → P) (H : a < b) : lt.by_cases H1 H2 H3 = H1 H :=
   begin
@@ -81,4 +77,38 @@ namespace nat
         exfalso, apply lt.irrefl, apply lt_of_le_of_lt H H'}
   end
 
+  definition code [reducible] [unfold 1 2] : ℕ → ℕ → Type₀
+  | code 0 0               := unit
+  | code (succ n) 0        := empty
+  | code 0 (succ m)        := empty
+  | code (succ n) (succ m) := code n m
+
+  definition refl : Πn, code n n
+  | refl 0 := star
+  | refl (succ n) := refl n
+
+  definition encode [unfold 3] {n m : ℕ} (p : n = m) : code n m :=
+  p ▸ refl n
+
+  definition decode : Π(n m : ℕ), code n m → n = m
+  | decode 0 0               := λc, idp
+  | decode 0 (succ l)        := λc, empty.elim c _
+  | decode (succ k) 0        := λc, empty.elim c _
+  | decode (succ k) (succ l) := λc, ap succ (decode k l c)
+
+  definition nat_eq_equiv (n m : ℕ) : (n = m) ≃ code n m :=
+  equiv.MK encode
+           !decode
+           begin
+             revert m, induction n, all_goals (intro m;induction m;all_goals intro c),
+               all_goals try contradiction,
+               induction c, reflexivity,
+               xrewrite [↑decode,-tr_compose,v_0],
+           end
+           begin
+             intro p, induction p, esimp, induction n,
+               reflexivity,
+               rewrite [↑decode,↑refl,v_0]
+           end
+
 end nat