2.4.8

src/HottBook/Chapter2.lagda.md

@@ -337,31 +337,23 @@ id-qinv = mkQinv id (λ _ → refl) (λ _ → refl)
 
 ```
 module example2∙4∙8 where
-  private
-    variable
-      A : Set
-      x y z : A
-
-  i : (p : x ≡ y) → qinv (p ∙_)
-  i p = mkQinv g forward backward
+  i : {A : Set} → {x y z : A} → (p : x ≡ y) → qinv (p ∙_)
+  i {A} {x} {y} {z} p = mkQinv g forward backward
     where
       g = (sym p) ∙_
       forward : (_∙_ p ∘ g) ∼ id
       forward q = lemma2∙1∙4.iv p (sym p) q ∙ ap (_∙ q) (lemma2∙1∙4.ii2 p) ∙ sym (lemma2∙1∙4.i2 q)
-      -- backward : (g ∘ (_∙_ p)) ∼ id
-      backward : {y z : A} → (q : {! y ≡ z  !}) → {!   !} ≡ q
-      -- sym p ∙ (q ∙ p) ≡ q
-      backward q = {!  !}
+      backward : (q : y ≡ z) → sym p ∙ (p ∙ q) ≡ q
+      backward q = lemma2∙1∙4.iv (sym p) p q ∙ ap (_∙ q) (lemma2∙1∙4.ii1 p) ∙ sym (lemma2∙1∙4.i2 q)
 
-  ii : (p : x ≡ y) → qinv (_∙ p)
-  ii p = mkQinv g forward backward
+  ii : {A : Set} → {x y z : A} → (p : x ≡ y) → qinv (_∙ p)
+  ii {A} {x} {y} {z} p = mkQinv g forward backward
     where
+      g : z ≡ y → z ≡ x
       g = _∙ (sym p)
       forward : (_∙ p ∘ g) ∼ id
-      -- (q ∙ sym(p)) ∙ p ≡ q
       forward q = sym (lemma2∙1∙4.iv q (sym p) p) ∙ ap (q ∙_) (lemma2∙1∙4.ii1 p) ∙ sym (lemma2∙1∙4.i1 q)
       backward : (g ∘ _∙ p) ∼ id
-      -- (q ∙ p) ∙ (sym p) ≡ q
       backward q = sym (lemma2∙1∙4.iv q p (sym p)) ∙ ap (q ∙_) (lemma2∙1∙4.ii2 p) ∙ sym (lemma2∙1∙4.i1 q)
 ```
 
@@ -1039,4 +1031,4 @@ theorem2∙15∙5 {X = X} {A = A} {B = B} = qinv-to-isequiv (mkQinv g forward ba
     backward : (f : (x : X) → A x × B x) → g (equation2∙15∙4 f) ≡ f
     backward f = funext λ x → refl
       where open axiom2∙9∙3
-```  
+```