From 7a9e1c7f4f820d05081ecb8cab7babcd8dc8c369 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 30 Mar 2016 11:43:41 +0100
Subject: [PATCH] chore(hott) fix sum proof by adding manual coercions

---
 hott/types/sum.hlean | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean
index dd132b0f8..a53909c7e 100644
--- a/hott/types/sum.hlean
+++ b/hott/types/sum.hlean
@@ -231,15 +231,15 @@ namespace sum
     esimp[unit_sum_equiv_cancel_map], apply sum.rec,
     { intro x, cases x with u Hu, esimp, apply sum.rec,
       { intro x, exfalso, cases x with u' Hu', apply empty_of_inl_eq_inr,
-        calc inl ⋆ = H⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹
-               ... = H⁻¹ (inl u') : ap H⁻¹ Hu'
-               ... = H⁻¹ (inl u) : {!is_prop.elim}
-               ... = H⁻¹ (H (inr _)) : {Hu⁻¹}
+        calc inl ⋆ = (to_fun H)⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹
+               ... = (to_fun H)⁻¹ (inl u') : ap (to_fun H)⁻¹ Hu'
+               ... = (to_fun H)⁻¹ (inl u) : {!is_prop.elim}
+               ... = (to_fun H)⁻¹ (H (inr _)) : {Hu⁻¹}
                ... = inr _ : to_left_inv H },
-      { intro x, cases x with b' Hb', esimp, cases sum.mem_cases (H⁻¹ (inr b)) with x x,
+      { intro x, cases x with b' Hb', esimp, cases sum.mem_cases ((to_fun H)⁻¹ (inr b)) with x x,
         { cases x with u' Hu', cases u', apply eq_of_inr_eq_inr,
           calc inr b' = H (inl ⋆)       : Hb'⁻¹
-                  ... = H (H⁻¹ (inr b)) : (ap (to_fun H) Hu')⁻¹
+                  ... = H ((to_fun H)⁻¹ (inr b)) : (ap (to_fun H) Hu')⁻¹
                   ... = inr b           : to_right_inv H (inr b)},
         { exfalso, cases x with a Ha, apply empty_of_inl_eq_inr,
           cases u, apply concat, apply Hu⁻¹, apply concat, rotate 1, apply !(to_right_inv H),
@@ -249,13 +249,13 @@ namespace sum
           apply concat, exact x.2⁻¹, apply Ha,
           intro x, cases x with a' Ha', esimp, apply eq_of_inr_eq_inr, apply Ha'⁻¹ ⬝ Ha } } },
     { intro x, cases x with b' Hb', esimp, apply eq_of_inr_eq_inr, refine Hb'⁻¹ ⬝ _,
-      cases sum.mem_cases (to_fun H⁻¹ᵉ (inr b)) with x x,
-      { cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ᵉ (inl ⋆)) with x x,
+      cases sum.mem_cases ((to_fun H)⁻¹ (inr b)) with x x,
+      { cases x with u Hu, esimp, cases sum.mem_cases ((to_fun H)⁻¹ (inl ⋆)) with x x,
         { cases x with u' Hu', exfalso, apply empty_of_inl_eq_inr,
-          calc inl ⋆ = H (H⁻¹ (inl ⋆))  : (to_right_inv H (inl ⋆))⁻¹
+          calc inl ⋆ = H ((to_fun H)⁻¹ (inl ⋆))  : (to_right_inv H (inl ⋆))⁻¹
                  ... = H (inl u')       : ap H Hu'
                  ... = H (inl u)        : by rewrite [is_prop.elim u' u]
-                 ... = H (H⁻¹ᵉ (inr b)) : ap H Hu⁻¹
+                 ... = H ((to_fun H)⁻¹ (inr b)) : ap H Hu⁻¹
                  ... = inr b            : to_right_inv H (inr b) },
       { cases x with a Ha, exfalso, apply empty_of_inl_eq_inr,
         apply concat, rotate 1, exact Hb',
@@ -267,8 +267,8 @@ namespace sum
             apply !(to_left_inv H)⁻¹ ⬝ Ha'',
           intro x, exfalso, cases x with a'' Ha'', apply empty_of_inl_eq_inr,
           apply Hu⁻¹ ⬝ Ha'', } },
-    { cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H,
-      exact sorry /-apply Ha'⁻¹-/ } }
+      { cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H,
+        apply Ha'⁻¹ } }
   end
 
   definition unit_sum_equiv_cancel : A ≃ B :=