diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index 56039f06b..5caa67659 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -77,24 +77,18 @@ namespace trunc
 
   section
   open prod.ops
-  -- definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
-  -- sorry
-  -- equiv.MK (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))
-  --          (λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, tr (x,y))))
-  --          sorry --(λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, idp)))
-  --          (λpp, trunc.rec_on pp (λp, prod.rec_on p (λx y, idp)))
-
-  -- begin
-  --   fapply equiv.MK,
-  --     apply sorry, --{exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))},
-  --     apply sorry, /-{intro p, cases p with xx yy,
-  --       apply (trunc.rec_on xx), intro x,
-  --       apply (trunc.rec_on yy), intro y, exact (tr (x,y))},-/
-  --     apply sorry, /-{intro p, cases p with xx yy,
-  --       apply (trunc.rec_on xx), intro x,
-  --       apply (trunc.rec_on yy), intro y, apply idp},-/
-  --     apply sorry --{intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp},
-  -- end
+  definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
+  begin
+    fapply equiv.MK,
+      {exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))},
+      {intro p, cases p with xx yy,
+        apply (trunc.rec_on xx), intro x,
+        apply (trunc.rec_on yy), intro y, exact (tr (x,y))},
+      {intro p, cases p with xx yy,
+        apply (trunc.rec_on xx), intro x,
+        apply (trunc.rec_on yy), intro y, apply idp},
+      {intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp}
+  end
   end
 
   /- Propositional truncation -/
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index b054de874..d32424ad8 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -148,25 +148,29 @@ namespace trunc
   protected definition code (n : trunc_index) (aa aa' : trunc n.+1 A) : n-Type :=
   trunc.rec_on aa (λa, trunc.rec_on aa' (λa', trunctype.mk' n (trunc n (a = a'))))
 
-  -- protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → code n aa aa' :=
-  -- trunc.rec_on aa (λa, trunc.rec_on aa' (λa' p, _))
+  protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → code n aa aa' :=
+  begin
+    intro p, cases p, apply (trunc.rec_on aa),
+    intro a, esimp [code,trunc.rec_on], exact (tr idp)
+  end
+
+  protected definition decode (n : trunc_index) (aa aa' : trunc n.+1 A) : code n aa aa' → aa = aa' :=
+  begin
+    eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa),
+    intro a a' x, esimp [code, trunc.rec_on] at x,
+    apply (trunc.rec_on x), intro p, exact (ap tr p)
+  end
 
   definition trunc_eq_equiv (n : trunc_index) (aa aa' : trunc n.+1 A)
     : aa = aa' ≃ code n aa aa' :=
   begin
     fapply equiv.MK,
-    { intro p, cases p, apply (trunc.rec_on aa),
-      intro a, esimp [code,trunc.rec_on], exact (tr idp)},
+    { apply encode},
+    { apply decode},
     { eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa),
       intro a a' x, esimp [code, trunc.rec_on] at x,
-      apply (trunc.rec_on x), intro p, exact (ap tr p)},
-    {
-      -- apply (trunc.rec_on aa'), apply (trunc.rec_on aa),
-      -- intro a a' x, esimp [code, trunc.rec_on] at x,
-      -- apply (trunc.rec_on x), intro p,
-      -- cases p, esimp [trunc.rec_on,eq.cases_on,compose,id], -- apply idp --?
-      apply sorry},
-    { intro p, cases p, apply (trunc.rec_on aa), intro a, apply sorry},
+      apply (trunc.rec_on x), intro p, cases p, exact idp},
+    { intro p, cases p, apply (trunc.rec_on aa), intro a, exact idp},
   end
 
   definition tr_eq_tr_equiv (n : trunc_index) (a a' : A)