From 43fb33491422f912e91b913de6f61c55da46ae0e Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 30 Apr 2015 20:45:31 -0400
Subject: [PATCH] feat(circle): prove loop != base

---
 hott/hit/circle.hlean    | 21 ++++++++++++++++++++-
 hott/types/default.hlean |  2 +-
 hott/types/types.md      |  1 +
 3 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean
index b51938a1c..0af9c618e 100644
--- a/hott/hit/circle.hlean
+++ b/hott/hit/circle.hlean
@@ -8,7 +8,7 @@ Authors: Floris van Doorn
 Declaration of the circle
 -/
 
-import .sphere
+import .sphere types.bool types.eq
 
 open eq suspension bool sphere_index equiv equiv.ops
 
@@ -130,4 +130,23 @@ namespace circle
     transport (elim_type Pbase Ploop) loop = Ploop :=
   by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_loop];apply cast_ua_fn
 
+  definition loop_neq_idp : loop ≠ idp :=
+  assume H : loop = idp,
+  have H2 : Π{A : Type₁} {a : A} (p : a = a), p = idp,
+    from λA a p, calc
+      p   = ap (circle.elim a p) loop : elim_loop
+      ... = ap (circle.elim a p) (refl base) : by rewrite H,
+  absurd !H2 eq_bnot_ne_idp
+
+  definition nonidp (x : circle) : x = x :=
+  circle.rec_on x loop
+    (calc
+      loop ▹ loop = loop⁻¹ ⬝ loop ⬝ loop : transport_eq_lr
+        ... = loop : by rewrite [con.left_inv, idp_con])
+
+  definition nonidp_neq_idp : nonidp ≠ (λx, idp) :=
+  assume H : nonidp = λx, idp,
+  have H2 : loop = idp, from apd10 H base,
+  absurd H2 loop_neq_idp
+
 end circle
diff --git a/hott/types/default.hlean b/hott/types/default.hlean
index 670e2106f..5c082671c 100644
--- a/hott/types/default.hlean
+++ b/hott/types/default.hlean
@@ -6,4 +6,4 @@ Module: types.default
 Authors: Floris van Doorn
 -/
 
-import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed
+import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed .function .trunc .bool
diff --git a/hott/types/types.md b/hott/types/types.md
index 9e7cc9cf1..454d6104c 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -3,6 +3,7 @@ hott.types
 
 Various datatypes.
 
+* [bool](bool.hlean)
 * [prod](prod.hlean)
 * [sigma](sigma.hlean)
 * [pi](pi.hlean)