6.3.2

src/CubicalHott/Chapter2.lagda.md

@@ -59,6 +59,14 @@ module ≡-Reasoning where
   _ ∎ = refl
 ```
 
+### Lemma 2.1.4
+
+```
+module lemma2∙1∙4 {l : Level} {A : Type l} where
+  iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
+  iii {x} {y} p i j = p j
+```
+
 ### Lemma 2.2.1
 
 {{#include CubicalHott.Chapter2Lemma221.md:ap}}

src/CubicalHott/Chapter6.lagda.md

@@ -4,6 +4,10 @@ module CubicalHott.Chapter6 where
 
 open import CubicalHott.Chapter1
 open import CubicalHott.Chapter2
+
+private
+  variable
+    l : Level
 ```
 
 ## 6.3 The interval
@@ -18,7 +22,21 @@ data Iv : Type where
 ### Lemma 6.3.1
 
 ```
+isContr : (A : Type l) → Type l
+isContr A = Σ A (λ a → (x : A) → a ≡ x)
+
 lemma6∙3∙1 : isContr Iv
+lemma6∙3∙1 = 1I , f
+  where
+    f : (x : Iv) → 1I ≡ x
+    f 0I = sym seg
+    f 1I = refl
+    f (seg i) j = {!   !}
+```
+
+### Lemma 6.3.2
+
+```
 ```
 
 ## 6.4 Circles and spheres

src/HottBook/Chapter2.lagda.md

@@ -185,6 +185,8 @@ transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
   → (b : B)
   → transport (λ _ → B) p b ≡ b
 transportconst {l₁} {l₂} {A} {x} {y} B refl b = refl
+
+{-# REWRITE transportconst #-}
 ```
 
 ### Equation 2.3.6

src/HottBook/Chapter3.lagda.md

@@ -481,7 +481,9 @@ Principle of unique choice
 --   → ((x : A) → isProp (P x))
 --   → ((x : A) → ∥ P x ∥)
 --   → (x : A) → P x
--- corollary3∙9∙2 assump1 assump2 x = {!   !}
+-- corollary3∙9∙2 {A = A} {P = P} assump1 assump2 x = 
+--   let rec = trunc-rec A (assump1 x) (λ y → {!assump2 x   !}) (∣ x ∣)
+--   in rec
 ```
 
 ## 3.11 Contractibility

src/HottBook/Chapter6.lagda.md

@@ -31,25 +31,60 @@ syntax dep-path P p u v = u ≡[ P , p ] v
 ## 6.3 The interval
 
 ```
-postulate
+module Interval where
+  data #I : Set where
+    #0 : #I
+    #1 : #I
+
   I : Set
+  I = #I
+
   0I : I
+  0I = #0
+
   1I : I
-  seg : 0I ≡ 1I
+  1I = #1
 
-record I-rec (B : Set) (b0 b1 : B) (s : b0 ≡ b1) : Set where
-  field
-    f : I → B
-    prop1 : f 0I ≡ b0
-    prop2 : f 1I ≡ b1
-    prop3 : apd f seg ≡ {! s  !}
+  postulate
+    seg : 0I ≡ 1I
 
-record I-ind (P : I → Set) (b0 : P 0I) (b1 : P 1I) (s : b0 ≡[ P , seg ] b1) : Set where
-  field
-    f : (x : I) → P x
-    prop1 : f 0I ≡ b0
-    prop2 : f 1I ≡ b1
-    prop3 : apd f seg ≡ {! s  !}
+  postulate
+    rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B
+
+    rec-Interval-1 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 0I ≡ b₀
+    rec-Interval-2 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 1I ≡ b₁
+
+  {-# REWRITE rec-Interval-1 #-}
+  {-# REWRITE rec-Interval-2 #-}
+
+  postulate
+    rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s
+  {-# REWRITE rec-Interval-3 #-}
+open Interval public
+```
+
+### Lemma 6.3.1
+
+```
+lemma6∙3∙1 : isContr I
+lemma6∙3∙1 = 1I , f
+  where
+    f : (x : I) → 1I ≡ x
+    f #0 = sym seg
+    f #1 = refl
+```
+
+### Lemma 6.3.2
+
+```
+lemma6∙3∙2 : {A B : Set} {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
+lemma6∙3∙2 {A = A} {B = B} {f = f} {g = g} p = apd q seg
+  where
+    p' : (x : A) → I → B
+    p' x = rec-Interval (f x) (g x) (p x)
+
+    q : I → (A → B)
+    q i x = p' x i
 ```
 
 ## 6.4 Circles and sphere
@@ -72,28 +107,30 @@ S¹-rec : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → (
 S¹-rec b l #base = b
 
 postulate
-  S¹-rec-loop : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → apd (S¹-rec b l) loop ≡ l
+  S¹-rec-loop : {P : S¹ → Set} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (S¹-rec b l) loop ≡ l
+
+{-# REWRITE S¹-rec-loop #-}
 ```
 
 ### Lemma 6.4.1
 
 ```
-lemma6∙4∙1 : loop ≢ refl
-lemma6∙4∙1 loop≡refl =
-  {!   !}
-  where
-    f : {A : Set} {x : A} {p : x ≡ x} → (S¹ → A)
-    f {A = A} {x = x} {p = p} s =
-      let p' = transportconst A loop x
-      in (S¹-rec x (p' ∙ p)) s
-    f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p
-    f-loop {x = x} = S¹-rec-loop x ?
+-- lemma6∙4∙1 : loop ≢ refl
+-- lemma6∙4∙1 loop≡refl =
+--   {!   !}
+--   where
+--     f : {A : Set} {x : A} {p : x ≡ x} → (S¹ → A)
+--     f {A = A} {x = x} {p = p} s =
+--       let p' = transportconst A loop x
+--       in (S¹-rec x (p' ∙ p)) s
+--     -- f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p
+--     -- f-loop {x = x} = S¹-rec-loop x ?
 
-    goal : ⊥
+--     goal : ⊥
 
-    goal2 : (A : Set l) (a : A) (p : a ≡ a) → isSet A 
-    goal = example3∙1∙9 (goal2 {!   !} {!   !} {!   !})
+--     goal2 : (A : Set l) (a : A) (p : a ≡ a) → isSet A 
+--     goal = example3∙1∙9 (goal2 {!   !} {!   !} {!   !})
 
-    -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl
-    goal2 A a p x y r s = {!   !}
+--     -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl
+--     goal2 A a p x y r s = {!   !}
 ```