Misc lemmas

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 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) 
+  (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 =
+  (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
+  ).fst

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

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
   =

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'))
   =

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)))