prove that n is surjective in the five lemma, closes #47

src/Misc/FiveLemma/FiveLemmaGroup.lagda.md

@@ -53,13 +53,11 @@ module _
   where
 
     sur : isSurjective' n
-    -- Let c′ be an element of C′.
     sur c' =
       let
         d' : ⟨ D' ⟩
         d' = t .fst c'
 
-        -- Since p is surjective, there exists an element d in D with p(d) = t(c′).
         pGroupIso = BijectionIso'→GroupIso p
         pIso = pGroupIso .fst
         pInv = Iso.inv pIso
@@ -169,8 +167,14 @@ module _
         s[m[b]]≡c'-n[c] : s .fst (m .fun .fst b) ≡ c'-n[c]
         s[m[b]]≡c'-n[c] = s[m[b]]≡s[b'] ∙ s[b']≡c'-n[c]
 
+        g[b] : ⟨ C ⟩
+        g[b] = g .fst b
+
+        g[b]+c : ⟨ C ⟩
+        g[b]+c = C .snd .GroupStr._·_ g[b] c
+
         n[g[b]] : ⟨ C' ⟩
-        n[g[b]] = n .fst (g .fst b)
+        n[g[b]] = n .fst g[b]
 
         n[g[b]]≡s[m[b]] : n[g[b]] ≡ s .fst (m .fun .fst b)
         n[g[b]]≡s[m[b]] = sym (sq2 b)
@@ -182,7 +186,10 @@ module _
         n[g[b]]+n[c]≡c' =
           let open GroupStr (C' .snd) in
           cong (_· n[c]) n[g[b]]≡c'-n[c] ∙ sym (·Assoc c' (inv n[c]) n[c]) ∙ cong (c' ·_) (·InvL n[c]) ∙ ·IdR c'
-      in c , {!   !}
+
+        n[g[b]+c]≡c' : n .fst g[b]+c ≡ c'
+        n[g[b]+c]≡c' = n .snd .pres· g[b] c ∙ n[g[b]]+n[c]≡c'
+      in g[b]+c , n[g[b]+c]≡c'
 
     mono : isMono n
     mono x = {!   !}