From 4af035f7131433059aa713b88ddabb267a1be9d5 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sun, 21 Jul 2024 14:12:39 -0500
Subject: [PATCH] agda hangs with 2.6.4.1 on Chapter2

---
 Makefile                       |  6 +--
 src/HottBook/Chapter2.lagda.md | 70 ++++++++++++++++++++--------------
 2 files changed, 44 insertions(+), 32 deletions(-)

diff --git a/Makefile b/Makefile
index ed631ea..94448f2 100644
--- a/Makefile
+++ b/Makefile
@@ -19,8 +19,8 @@ build-to-html:
 .PHONY: html/src/generated/Progress.md
 
 html/src/generated/Progress.md:
-	# nu scripts/build-table
-	touch $@
+	nu scripts/build-table
+	# touch $@
 
 html/book/Progress.html: html/src/generated/Progress.md
 	pandoc \
@@ -43,4 +43,4 @@ deploy: build-book html/book/progress/index.html
 	rsync -azr html/book/ root@veil:/home/blogDeploy/public/research
 
 .PHONY: build-book build-to-html deploy
-    # -not \( -path src/CubicalHott -prune \) \
\ No newline at end of file
+    # -not \( -path src/CubicalHott -prune \) \
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 8c8fc20..bb1150d 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -336,7 +336,33 @@ id-qinv = mkQinv id (λ _ → refl) (λ _ → refl)
 ### Example 2.4.8
 
 ```
+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
+    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 = {!  !}
+
+  ii : (p : x ≡ y) → qinv (_∙ p)
+  ii p = mkQinv g forward backward
+    where
+      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)
 ```
 
 ### Example 2.4.9
@@ -451,36 +477,22 @@ module lemma2∙4∙12 where
 ### Definition 2.5.1
 
 ```
--- definition2∙5∙1 : {B C : Set} {b b' : B} {c c' : C}
---   → ((b , c) ≡ (b' , c')) ≃ ((b ≡ b') × (c ≡ c'))
--- definition2∙5∙1 {B} {C} {b} {b'} {c} {c'} =
---   let
---     open Σ
+definition2∙5∙1 : {B C : Set} {b b' : B} {c c' : C}
+  → ((b , c) ≡ (b' , c')) ≃ ((b ≡ b') × (c ≡ c'))
+definition2∙5∙1 {B = B} {C = C} {b = b} {b' = b'} {c = c} {c' = c'} =
+  f , qinv-to-isequiv (mkQinv g forward backward)
+  where
+    f : {b b' : B} {c c' : C} → ((b , c) ≡ (b' , c')) → ((b ≡ b') × (c ≡ c'))
+    f p = ap fst p , ap snd p
 
---     f : ((b , c) ≡ (b' , c')) → ((b ≡ b') × (c ≡ c')) 
---     f p = ap fst p , ap snd p
+    g : {b b' : B} {c c' : C} → ((b ≡ b') × (c ≡ c')) → ((b , c) ≡ (b' , c'))
+    g (refl , refl) = refl
 
---     g : ((b ≡ b') × (c ≡ c')) → ((b , c) ≡ (b' , c'))
---     g p =
---       let (p1 , p2) = p in
---       J (λ x1 y1 p1 → (x1 , c) ≡ (y1 , c'))
---       (λ x1 → ap (λ p → (x1 , p)) p2) b b' p1
-
---     open ≡-Reasoning
-
---     forward : (g ∘ f) ∼ id
---     forward x =
---       J (λ x1 y1 p1 → (g ∘ f) {! !} ≡ id {!   !})
---       (λ x1 → {!   !}) (b , c) (b' , c') x
-
---     backward : (f ∘ g) ∼ id
---     backward x = 
---       let (p1 , p2) = x in
---       begin
---         f (g (p1 , p2)) ≡⟨ {!   !} ⟩
---         f (J (λ x1 y1 p1 → (x1 , c) ≡ (y1 , c')) (λ x1 → ap (λ p → (x1 , p)) p2) b b' p1) ≡⟨ {!   !} ⟩
---         id x ∎
---   in f , qinv-to-isequiv (mkQinv g backward forward)
+    forward : {b b' : B} {c c' : C} → (f {b} {b'} {c} {c'} ∘ g {b} {b'} {c} {c'}) ∼ id
+    forward (refl , refl) = refl
+    
+    backward : {b b' : B} {c c' : C} → (g {b} {b'} {c} {c'} ∘ f {b} {b'} {c} {c'}) ∼ id
+    backward refl = refl 
 ```
 
 ## 2.6 Cartesian product types
@@ -1027,4 +1039,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
-``` 
\ No newline at end of file
+```  
\ No newline at end of file