feat(types/eq): add general encode-decode method

hott/types/eq.hlean

@@ -7,13 +7,14 @@ Partially ported from Coq HoTT
 Theorems about path types (identity types)
 -/
 
-open eq sigma sigma.ops equiv is_equiv equiv.ops
+import types.sigma
+open eq sigma sigma.ops equiv is_equiv equiv.ops is_trunc
 
 -- TODO: Rename transport_eq_... and pathover_eq_... to eq_transport_... and eq_pathover_...
 
 namespace eq
   /- Path spaces -/
-
+  section
   variables {A B : Type} {a a₁ a₂ a₃ a₄ a' : A} {b b1 b2 : B} {f g : A → B} {h : B → A}
             {p p' p'' : a₁ = a₂}
 
@@ -432,6 +433,63 @@ namespace eq
 
   -- a lot of this library still needs to be ported from Coq HoTT
 
+  -- encode decode method
+
+  open is_trunc
+  definition encode_decode_method' (a₀ a : A) (code : A → Type) (c₀ : code a₀)
+    (decode : Π(a : A) (c : code a), a₀ = a)
+    (encode_decode : Π(a : A) (c : code a), c₀ =[decode a c] c)
+    (decode_encode : decode a₀ c₀ = idp) : (a₀ = a) ≃ code a :=
+  begin
+    fapply equiv.MK,
+    { intro p, exact p ▸ c₀},
+    { apply decode},
+    { intro c, apply tr_eq_of_pathover, apply encode_decode},
+    { intro p, induction p, apply decode_encode},
+  end
+
+  end
+
+  section
+    parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a))
+      (p : (center (Σa, code a)).1 = a₀)
+    include p
+    definition encode {a : A} (q : a₀ = a) : code a :=
+    (p ⬝ q) ▸ (center (Σa, code a)).2
+
+    definition decode' {a : A} (c : code a) : a₀ = a :=
+    (is_hprop.elim ⟨a₀, encode idp⟩ ⟨a, c⟩)..1
+
+    definition decode {a : A} (c : code a) : a₀ = a :=
+    (decode' (encode idp))⁻¹ ⬝ decode' c
+
+    definition total_space_method (a : A) : (a₀ = a) ≃ code a :=
+    begin
+      fapply equiv.MK,
+      { exact encode},
+      { exact decode},
+      { intro c,
+        unfold [encode, decode, decode'],
+        induction p, esimp, rewrite [is_hprop_elim_self,▸*,+idp_con], apply tr_eq_of_pathover,
+        eapply @sigma.rec_on _ _ (λx, x.2 =[(is_hprop.elim ⟨x.1, x.2⟩ ⟨a, c⟩)..1] c)
+          (center (sigma code)), -- BUG(?): induction fails
+        intro a c, apply eq_pr2},
+      { intro q, induction q, esimp, apply con.left_inv, },
+    end
+  end
+
+  definition encode_decode_method {A : Type} (a₀ a : A) (code : A → Type) (c₀ : code a₀)
+    (decode : Π(a : A) (c : code a), a₀ = a)
+    (encode_decode : Π(a : A) (c : code a), c₀ =[decode a c] c) : (a₀ = a) ≃ code a :=
+  begin
+    fapply total_space_method,
+    { fapply @is_contr.mk,
+      { exact ⟨a₀, c₀⟩},
+      { intro p, fapply sigma_eq,
+          apply decode, exact p.2,
+        apply encode_decode}},
+    { reflexivity}
+  end
 
 
 end eq

hott/types/sigma.hlean

@@ -9,7 +9,7 @@ Theorems about sigma-types (dependent sums)
 
 import types.prod
 
-open eq sigma sigma.ops equiv is_equiv function
+open eq sigma sigma.ops equiv is_equiv function is_trunc
 
 namespace sigma
   variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
@@ -35,7 +35,7 @@ namespace sigma
   definition sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) : u = v :=
   by induction u; induction v; exact (dpair_eq_dpair p q)
 
-  definition eq_pr1 (p : u = v) : u.1 = v.1 :=
+  definition eq_pr1 [unfold 5] (p : u = v) : u.1 = v.1 :=
   ap pr1 p
 
   postfix `..1`:(max+1) := eq_pr1
@@ -162,8 +162,8 @@ namespace sigma
   by induction p; induction bc; reflexivity
 
   /- The special case when the second variable doesn't depend on the first is simpler. -/
-  definition sigma_transport_nondep {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b)
+  definition sigma_transport_nondep {B : Type} {C : A → B → Type} (p : a = a')
-      : p ▸ bc = ⟨bc.1, p ▸ bc.2⟩ :=
+    (bc : Σ(b : B), C a b) : p ▸ bc = ⟨bc.1, p ▸ bc.2⟩ :=
   by induction p; induction bc; reflexivity
 
   /- Or if the second variable contains a first component that doesn't depend on the first. -/
@@ -242,7 +242,7 @@ namespace sigma
   -- by induction u; induction v; apply ap_sigma_functor_eq_dpair
 
   /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/
-  open is_trunc
+
   definition is_equiv_pr1 [instance] (B : A → Type) [H : Π a, is_contr (B a)]
       : is_equiv (@pr1 A B) :=
   adjointify pr1