From 8a1c75a63875dc60c12aff8a861714d40ead441b Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <a.gryzlov@adform.com>
Date: Tue, 6 Nov 2018 14:38:38 +0200
Subject: [PATCH 1/5] print mismatched names in Quote

---
 src/core/Quote.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/core/Quote.ml b/src/core/Quote.ml
index 41ae779e7..ca0a598e6 100644
--- a/src/core/Quote.ml
+++ b/src/core/Quote.ml
@@ -2,6 +2,7 @@ open Domain
 open RedBasis
 open Bwd
 open BwdNotation
+open Name
 
 module D = Domain
 
@@ -399,12 +400,12 @@ struct
       if info0.name = info1.name && info0.twin = info1.twin && info0.ushift = info1.ushift then
         Tm.Var {name = info0.name; twin = info0.twin; ushift = info0.ushift}, stk
       else
-        failwith "global variable name mismatch"
+        failwith @@ "global variable name mismatch: " ^ to_string info0.name ^ " <> " ^ to_string info1.name
     | Meta meta0, Meta meta1 ->
       if meta0.name = meta1.name && meta0.ushift = meta1.ushift then
         Tm.Meta {name = meta0.name; ushift = meta0.ushift}, stk
       else
-        failwith "global variable name mismatch"
+        failwith @@ "global variable name mismatch: " ^ to_string meta0.name ^ " <> " ^ to_string meta1.name
 
     | NHComAtType info0, NHComAtType info1 ->
       let tr, tr' = equate_dir env info0.dir info1.dir in

From 23bfe199edd5d27bd49299cd8843cd205d587c0a Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <a.gryzlov@adform.com>
Date: Wed, 7 Nov 2018 18:28:19 +0200
Subject: [PATCH 2/5] fix after review

---
 src/core/Quote.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/core/Quote.ml b/src/core/Quote.ml
index ca0a598e6..344b49bfd 100644
--- a/src/core/Quote.ml
+++ b/src/core/Quote.ml
@@ -2,7 +2,6 @@ open Domain
 open RedBasis
 open Bwd
 open BwdNotation
-open Name
 
 module D = Domain
 
@@ -400,12 +399,12 @@ struct
       if info0.name = info1.name && info0.twin = info1.twin && info0.ushift = info1.ushift then
         Tm.Var {name = info0.name; twin = info0.twin; ushift = info0.ushift}, stk
       else
-        failwith @@ "global variable name mismatch: " ^ to_string info0.name ^ " <> " ^ to_string info1.name
+        failwith @@ "global variable name mismatch: " ^ Name.to_string info0.name ^ " <> " ^ Name.to_string info1.name
     | Meta meta0, Meta meta1 ->
       if meta0.name = meta1.name && meta0.ushift = meta1.ushift then
         Tm.Meta {name = meta0.name; ushift = meta0.ushift}, stk
       else
-        failwith @@ "global variable name mismatch: " ^ to_string meta0.name ^ " <> " ^ to_string meta1.name
+        failwith @@ "global variable name mismatch: " ^ Name.to_string meta0.name ^ " <> " ^ Name.to_string meta1.name
 
     | NHComAtType info0, NHComAtType info1 ->
       let tr, tr' = equate_dir env info0.dir info1.dir in

From 58e4acef5504de3e1d9109a85d087b4942105aab Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <a.gryzlov@adform.com>
Date: Thu, 15 Nov 2018 23:50:56 +0200
Subject: [PATCH 3/5] misc lemmas

---
 library/basics/hedberg.red   | 25 +++++++++++++++++++++++++
 library/paths/bool.red       | 18 ++++++++++++++++++
 library/paths/hlevel.red     | 10 +++++++++-
 library/paths/sigma.red      | 24 +++++++++++++++++++++++-
 library/paths/truncation.red | 14 ++++++++++++++
 5 files changed, 89 insertions(+), 2 deletions(-)
 create mode 100644 library/paths/truncation.red

diff --git a/library/basics/hedberg.red b/library/basics/hedberg.red
index 9b1613b58..faa9518a8 100644
--- a/library/basics/hedberg.red
+++ b/library/basics/hedberg.red
@@ -1,4 +1,5 @@
 import prelude
+import basics.retract
 import data.void
 import data.or
 
@@ -46,3 +47,27 @@ def paths-stable→set (A : type) (st : (x y : A) → stable (path A x y)) : is-
 -- Hedberg's theorem for decidable path types
 def discrete→set (A : type) (d : discrete A) : is-set A =
   paths-stable→set A (λ x y → dec→stable (path A x y) (d x y))
+
+def mere-relation/set-equiv 
+  (A : type) (R : A → A → type) 
+  (R/prop : (x y : A) → is-prop (R x y))
+  (R/refl : (x : A) → R x x) 
+  (R/id : (x y : A) → R x y → path A x y) 
+  : (is-set A) × ((x y : A) → equiv (R x y) (path A x y))
+  = 
+  let eq = path-retract/equiv A R (λ a b → 
+    ( R/id a b
+    , λ p → coe 0 1 (R/refl a) in λ j → R a (p j)
+    , λ rab → R/prop a b (coe 0 1 (R/refl a) in λ j → R a (R/id a b rab j)) rab
+    )) in
+  ( λ x y → coe 0 1 (R/prop x y) in λ j → is-prop (ua _ _ (eq x y) j)
+  , eq 
+  )
+
+-- Hedberg's theorem is a corollary of above
+def paths-stable→set/alt (A : type) (st : (x y : A) → stable (path A x y)) : is-set A =
+  (mere-relation/set-equiv A (λ x y → neg (neg (path A x y)))
+    (λ x y → neg/prop (neg (path A x y)))
+    (λ _ np → np refl)
+    st
+).fst
\ No newline at end of file
diff --git a/library/paths/bool.red b/library/paths/bool.red
index db3fd1bd1..3eb36ff88 100644
--- a/library/paths/bool.red
+++ b/library/paths/bool.red
@@ -3,6 +3,7 @@ import data.void
 import data.unit
 import data.bool
 import basics.isotoequiv
+import basics.hedberg
 
 def bool-path/code : bool → bool → type =
   elim [
@@ -24,3 +25,20 @@ def not/equiv : equiv bool bool =
 
 def not/path : path^1 type bool bool =
   ua _ _ not/equiv
+
+def bool/discrete : discrete bool = 
+  elim [
+  | tt →
+    elim [
+    | tt → inl refl
+    | ff → inr (not/neg ff)
+    ]
+  | ff →
+    elim [
+    | tt → inr (not/neg tt)
+    | ff → inl refl
+    ]
+  ]
+
+def bool/set : is-set bool =
+discrete→set bool bool/discrete
\ No newline at end of file
diff --git a/library/paths/hlevel.red b/library/paths/hlevel.red
index c7d87e74a..12836f369 100644
--- a/library/paths/hlevel.red
+++ b/library/paths/hlevel.red
@@ -1,7 +1,15 @@
 import prelude
+import data.unit
+import basics.isotoequiv
 import paths.sigma
 import paths.pi
 
+def prop/unit (A : type) (A/prop : is-prop A) (x0 : A) : equiv A unit = 
+  iso→equiv A unit (λ _ → ★, λ _ → x0, unit/prop ★, A/prop x0)
+
+def prop/equiv (P Q : type) (P/prop : is-prop P) (Q/prop : is-prop Q) (f : P → Q) (g : Q → P) : equiv P Q = 
+  iso→equiv P Q (f, g, λ p → Q/prop (f (g p)) p, λ q → P/prop (g (f q)) q)
+
 def contr-equiv (A B : type) (A/contr : is-contr A) (B/contr : is-contr B)
   : equiv A B
   =
@@ -32,4 +40,4 @@ def has-hlevel/prop : (l : hlevel) (A : type) → is-prop (has-hlevel l A) =
     | hsuc (l → l/ih) → λ A A/level A/level' i a a' →
       l/ih (path A a a') (A/level a a') (A/level' a a') i
     ]
-  ]
+]
\ No newline at end of file
diff --git a/library/paths/sigma.red b/library/paths/sigma.red
index 44fcd1722..6a9dff90e 100644
--- a/library/paths/sigma.red
+++ b/library/paths/sigma.red
@@ -2,6 +2,28 @@ import prelude
 import basics.isotoequiv
 import basics.retract
 
+def sigma/assoc (A : type) (B : A → type) (C : ((x : A) × B x) → type) 
+  : equiv ((x : A) × (y : B x) × C (x, y)) ((p : ((x : A) × B x)) × C p) 
+  = 
+  ( λ x → ((x.fst, x.snd.fst), x.snd.snd)
+  , λ b → ( ((b.fst.fst, b.fst.snd, b.snd), refl)
+          , λ c i → 
+            ( ((c.snd i).fst.fst, (c.snd i).fst.snd, (c.snd i).snd)
+            , λ j → weak-connection/or _ (c.snd) i j
+            )
+          )
+  )
+
+def sigma/contr/equiv/fst (A : type) (P : A → type) (P/contr : (x : A) → is-contr (P x)) 
+  : equiv ((x : A) × P x) A 
+  = 
+  iso→equiv ((x : A) × P x) A 
+    ( λ s → s.fst
+    , λ x → (x, (P/contr x).fst)
+    , refl
+    , λ s i → (s.fst, symm _ ((P/contr (s.fst)).snd (s.snd)) i)
+    )  
+
 def sigma/path (A : type) (B : A → type) (a : A) (b : B a) (a' : A) (b' : B a')
   : equiv ((p : path A a a') × pathd (λ i → B (p i)) b b') (path ((a : A) × B a) (a,b) (a',b'))
   =
@@ -56,4 +78,4 @@ def subtype/path
   λ i →
   ( P i
   , prop→prop-over (λ i → B (P i)) (B/prop (P 1)) (u.snd) (v.snd) i
-  )
+)
\ No newline at end of file
diff --git a/library/paths/truncation.red b/library/paths/truncation.red
new file mode 100644
index 000000000..0d4fc9813
--- /dev/null
+++ b/library/paths/truncation.red
@@ -0,0 +1,14 @@
+import prelude
+import basics.isotoequiv
+import data.truncation
+import paths.hlevel
+
+def prop/trunc (A : type) (A/prop : is-prop A) : equiv A (trunc A) = 
+  prop/equiv _ _ A/prop (trunc/prop A) 
+    (λ x → ret x) (elim [ ret a → a | glue (x → x/ih) (y → y/ih) i → A/prop x/ih y/ih i ])
+
+def unique-choice (A : type) (P : A → type) 
+  (P/prop : (x : A) → is-prop (P x)) (P/trunc : (x : A) → trunc (P x)) 
+  : (x : A) → P x 
+  =
+  λ x → coe 0 1 (P/trunc x) in symm^1 _ (ua _ _ (prop/trunc (P x) (P/prop x)))

From 6539b427f27b283d8b1cea6d5fb3e606c69aa07d Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <a.gryzlov@adform.com>
Date: Thu, 15 Nov 2018 23:53:27 +0200
Subject: [PATCH 4/5] fix endings

---
 library/basics/hedberg.red | 2 +-
 library/paths/bool.red     | 2 +-
 library/paths/hlevel.red   | 2 +-
 library/paths/sigma.red    | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/basics/hedberg.red b/library/basics/hedberg.red
index faa9518a8..0c8264c65 100644
--- a/library/basics/hedberg.red
+++ b/library/basics/hedberg.red
@@ -70,4 +70,4 @@ def paths-stable→set/alt (A : type) (st : (x y : A) → stable (path A x y)) :
     (λ x y → neg/prop (neg (path A x y)))
     (λ _ np → np refl)
     st
-).fst
\ No newline at end of file
+  ).fst
diff --git a/library/paths/bool.red b/library/paths/bool.red
index 3eb36ff88..dbdd736c6 100644
--- a/library/paths/bool.red
+++ b/library/paths/bool.red
@@ -41,4 +41,4 @@ def bool/discrete : discrete bool =
   ]
 
 def bool/set : is-set bool =
-discrete→set bool bool/discrete
\ No newline at end of file
+  discrete→set bool bool/discrete
diff --git a/library/paths/hlevel.red b/library/paths/hlevel.red
index 12836f369..ac448f2d6 100644
--- a/library/paths/hlevel.red
+++ b/library/paths/hlevel.red
@@ -40,4 +40,4 @@ def has-hlevel/prop : (l : hlevel) (A : type) → is-prop (has-hlevel l A) =
     | hsuc (l → l/ih) → λ A A/level A/level' i a a' →
       l/ih (path A a a') (A/level a a') (A/level' a a') i
     ]
-]
\ No newline at end of file
+  ]
diff --git a/library/paths/sigma.red b/library/paths/sigma.red
index 6a9dff90e..f66cec63e 100644
--- a/library/paths/sigma.red
+++ b/library/paths/sigma.red
@@ -78,4 +78,4 @@ def subtype/path
   λ i →
   ( P i
   , prop→prop-over (λ i → B (P i)) (B/prop (P 1)) (u.snd) (v.snd) i
-)
\ No newline at end of file
+  )

From fde70907e75cbf600b84fd6da8531bd4b7460ade Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <a.gryzlov@adform.com>
Date: Fri, 23 Nov 2018 19:04:16 +0200
Subject: [PATCH 5/5] rename

---
 library/basics/hedberg.red | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/basics/hedberg.red b/library/basics/hedberg.red
index 0c8264c65..6562a7768 100644
--- a/library/basics/hedberg.red
+++ b/library/basics/hedberg.red
@@ -48,7 +48,7 @@ def paths-stable→set (A : type) (st : (x y : A) → stable (path A x y)) : is-
 def discrete→set (A : type) (d : discrete A) : is-set A =
   paths-stable→set A (λ x y → dec→stable (path A x y) (d x y))
 
-def mere-relation/set-equiv 
+def hrel/set-equiv 
   (A : type) (R : A → A → type) 
   (R/prop : (x y : A) → is-prop (R x y))
   (R/refl : (x : A) → R x x) 
@@ -66,7 +66,7 @@ def mere-relation/set-equiv
 
 -- Hedberg's theorem is a corollary of above
 def paths-stable→set/alt (A : type) (st : (x y : A) → stable (path A x y)) : is-set A =
-  (mere-relation/set-equiv A (λ x y → neg (neg (path A x y)))
+  (hrel/set-equiv A (λ x y → neg (neg (path A x y)))
     (λ x y → neg/prop (neg (path A x y)))
     (λ _ np → np refl)
     st