feat(hott/init): add proof for Hedberg's theorem

hott/init/default.hlean

@@ -10,3 +10,4 @@ import init.bool init.num init.priority init.relation init.wf
 import init.types.sigma init.types.prod init.types.empty
 import init.trunc init.path init.equiv
 import init.axioms.ua init.axioms.funext init.axioms.funext_from_ua
+import init.hedberg

hott/init/hedberg.hlean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+Hedberg's Theorem: every type with decidable equality is a hset
+-/
+prelude
+import init.nat init.trunc
+open eq eq.ops nat truncation sigma.ops
+
+-- TODO(Leo): move const coll and path_coll to a different file?
+private definition const {A B : Type} (f : A → B) := ∀ x y, f x = f y
+private definition coll (A : Type) := Σ f : A → A, const f
+private definition path_coll (A : Type) := ∀ x y : A, coll (x = y)
+
+context
+  parameter  {A : Type}
+  hypothesis (h : decidable_eq A)
+  variables  {x y : A}
+
+  private definition pc : path_coll A :=
+  λ a b, decidable.rec_on (h a b)
+    (λ p  : a = b,   ⟨(λ q, p), λ q r, rfl⟩)
+    (λ np : ¬ a = b, ⟨(λ q, q), λ q r, absurd q np⟩)
+
+  private definition f : x = y → x = y :=
+  sigma.rec_on (pc x y) (λ f c, f)
+
+  private definition f_const (p q : x = y) : f p = f q :=
+  sigma.rec_on (pc x y) (λ f c, c p q)
+
+  private definition aux (p : x = y) : p = (f (refl x))⁻¹ ⬝ (f p) :=
+  have aux : refl x = (f (refl x))⁻¹ ⬝ (f (refl x)), from
+    eq.rec_on (f (refl x)) rfl,
+  eq.rec_on p aux
+
+  definition is_hset_of_decidable_eq : is_hset A :=
+  is_hset.mk A (λ x y p q, calc
+   p   = (f (refl x))⁻¹ ⬝ (f p) : aux
+   ... = (f (refl x))⁻¹ ⬝ (f q) : f_const
+   ... = q                      : aux)
+end
+
+instance [persistent] is_hset_of_decidable_eq