update

src/HottBook/Chapter1.lagda.md

@@ -130,7 +130,7 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 
 ```
 infix 3 ¬_
-¬_ : {l : Level} → (A : Set l) → Set l
+¬_ : ∀ {l : Level} (A : Set l) → Set l
 ¬_ {l} A = A → ⊥ {l}
 ```
 

src/HottBook/Chapter2.lagda.md

@@ -344,7 +344,7 @@ lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} p = let
 ### Definition 2.4.6
 
 ```
-record qinv {l : Level} {A B : Set l} (f : A → B) : Set l where
+record qinv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) : Set (l1 ⊔ l2) where
   constructor mkQinv
   field
     g : B → A
@@ -355,7 +355,7 @@ record qinv {l : Level} {A B : Set l} (f : A → B) : Set l where
 ### Example 2.4.7
 
 ```
-id-qinv : {l : Level} {A : Set l} → qinv {l} {A} id
+id-qinv : {l : Level} {A : Set l} → qinv {l} {l} {A} {A} id
 id-qinv = mkQinv id (λ _ → refl) (λ _ → refl)
 ```
 
@@ -396,7 +396,7 @@ record isequiv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) : Set (l1
 ```
 
 ```
-qinv-to-isequiv : {l : Level} {A B : Set l}
+qinv-to-isequiv : {l1 l2 : Level} {A : Set l1} {B : Set l2}
   → {f : A → B}
   → qinv f
   → isequiv f
@@ -667,25 +667,47 @@ equation2∙9∙4 {l1} {l2} {X} {x1} {x2} {A} {B} f p =
   (λ x3 f1 → refl) x1 x2 p f
 ```
 
+### Equation 2.9.5
+
+```
+module equation2∙9∙5 {X : Set} {x1 x2 : X} where
+  Π : (A : X → Set) → (B : (x : X) → A x → Set) → X → Set
+  Π A B x = (a : A x) → B x a
+
+  hat : {A : X → Set} → (B : (x : X) → A x → Set) → (Σ X A) → Set
+  hat B (fst , snd) = B fst snd
+
+  --- I have no idea where this goes but this definitely needs to exist
+  pair-≡ : {A : Set} {B : A → Set} {a1 a2 : A} {b1 : B a1} {b2 : B a2}
+    → (p : a1 ≡ a2) → (transport B p b1 ≡ b2) → (a1 , b1) ≡ (a2 , b2)
+  pair-≡ refl refl = refl
+
+  equation2∙9∙5 : (A : X → Set)
+    → (B : (x : X) → A x → Set)
+    → (f : (a : A x1) → B x1 a)
+    → (p : x1 ≡ x2)
+    → (a : A x2)
+    → transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡ (sym p) refl)) (f (transport A (sym p) a))
+  equation2∙9∙5 A B f p a =
+    J (λ x1' x2' p' → (f' : (a : A x1') → B x1' a) → (a' : A x2') → transport (Π A B) p' f' a' ≡ transport (hat B) (sym (pair-≡ (sym p') refl)) (f' (transport A (sym p') a')))
+      (λ x' f' a' → refl) x1 x2 p f a
+```
+
 ### Lemma 2.9.6
 
 ```
--- lemma2∙9∙6 : {X : Set} {A B : X → Set} {x y : X}
+-- module lemma2∙9∙6 {X : Set} {A B : X → Set} {x y : X} where
---   → (p : x ≡ y)
+--   P : (x : X) → Set
---   → (f : A x → B x)
+--   P x = A x → B x
---   → (g : A y → B y)
---   → 
---     let P x = A x → B x in
---     (transport P p f ≡ g) ≃ ((a : A x) → transport B p (f a) ≡ g (transport A p a))
--- lemma2∙9∙6 {X} {A} {B} {x} {y} p f g =
---   let
---     P x = A x → B x
 
---     F : (x1 : X) → (f1 : A x1 → B x1) → (g1 : A x1 → B x1) → (transport P refl f1 ≡ g1) → ((a : A x1) → transport B refl (f1 a) ≡ g1 (transport A refl a))
+--   lemma2∙9∙6 : (p : x ≡ y)
---     F x f g p a = {! !}
+--     → (f : A x → B x)
---   in
+--     → (g : A y → B y)
---   J (λ x1 y1 p1 → (f1 : A x1 → B x1) → (g1 : A y1 → B y1) → (transport P p1 f1 ≡ g1) ≃ ((a : A x1) → transport B p1 (f1 a) ≡ g1 (transport A p1 a))) 
+--     → (transport P p f ≡ g) ≃ ((a : A x) → transport B p (f a) ≡ g (transport A p a))
---     (λ x1 f1 g1 → F x1 f1 g1 , qinv-to-isequiv (mkQinv {!   !} {!   !} {!   !})) x y p f g
+--   lemma2∙9∙6 p f g = func , qinv-to-isequiv (mkQinv {!   !} {!   !} {!   !})
+--     where
+--       func : (transport P p f ≡ g) → (a : A x) → transport B p (f a) ≡ g (transport A p a)
+--       func p1 a = J (λ x y p' → {!   !} ≡ y (transport A {!   !} a)) {!   !} (transport P p f) g p1
 ```
 
 ## 2.10 Universes and the univalence axiom
@@ -710,17 +732,18 @@ idtoeqv {l} {A} {B} p = J C c A B p
 ```
 module axiom2∙10∙3 where
   postulate
-    -- ua-eqv : {l1 l2 : Level} {A : Set l1} {B : Set l2} → (A ≃ B) ≃ (A ≡ B)
-
     ua : {l : Level} {A B : Set l} → (A ≃ B) → (A ≡ B)
 
-  -- forward : {A B : Set} → (eqv @ (f , f-eqv) : A ≃ B) → (x : A) → transport id (ua eqv) x ≡ f x
+    forward : {l : Level} {A B : Set l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
-  -- forward eqv x = {!   !}
+    -- forward eqv = {!   !}
 
-  -- ua-refl : {A : Set} → refl ≡ ua (lemma2∙4∙12.id-equiv A)
+    backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
-  -- ua-refl = {!   !}
+    -- backward p = {!   !}
 
-open axiom2∙10∙3
+  ua-eqv : {l : Level} {A : Set l} {B : Set l} → (A ≃ B) ≃ (A ≡ B)
+  ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
+
+open axiom2∙10∙3 hiding (forward; backward)
 ```
 
 ### Lemma 2.10.5
@@ -860,7 +883,7 @@ theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} p q =
 ### Theorem 2.12.5
 
 ```
-module 2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where
+module theorem2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where
   code : A + B → Set l
   code (inl a) = a₀ ≡ a
   code (inr b) = ⊥
@@ -911,7 +934,7 @@ remark2∙12∙6 p = genBot tt
 _For all $m, n : N$ we have $(m = n) \simeq \texttt{code}(m, n)$._
 
 ```
-module 2∙13∙1 where
+module theorem2∙13∙1 where
   open ≡-Reasoning
 
   code : ℕ → ℕ → Set

src/HottBook/Chapter3.lagda.md

@@ -1,3 +1,6 @@
+<details>
+  <summary>Imports</summary>
+
 ```
 module HottBook.Chapter3 where
 
@@ -5,12 +8,13 @@ open import Agda.Primitive
 open import HottBook.Chapter1
 open import HottBook.Chapter1Util
 open import HottBook.Chapter2
-open import HottBook.Chapter3Definition331
+open import HottBook.Chapter3Definition331 public
-open import HottBook.Chapter3Lemma333
+open import HottBook.Chapter3Lemma333 public
 open import HottBook.Util
-
 ```
 
+</details>
+
 ## 3.1 Sets and n-types
 
 ### Definition 3.1.1
@@ -30,7 +34,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ### Example 3.1.3
 
 ```
-⊥-is-Set : isSet ⊥
+⊥-is-Set : ∀ {l} → isSet (⊥ {l})
 ⊥-is-Set () () p q
 ```
 
@@ -44,7 +48,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ### Example 3.1.9
 
 ```
-example3∙1∙9 : ¬ (isSet Set)
+example3∙1∙9 : ∀ {l : Level} → ¬_ {lsuc l} (isSet (Set l))
 example3∙1∙9 p = remark2∙12∙6 lol
   where
     open axiom2∙10∙3
@@ -55,13 +59,13 @@ example3∙1∙9 p = remark2∙12∙6 lol
     bogus : id ≡ neg
     bogus =
       let
-        helper : f-path ≡ refl
+        -- helper : f-path ≡ refl
-        helper = p 𝟚 𝟚 f-path refl
+        -- helper = p 𝟚 𝟚 f-path refl
 
         a = ap
 
-        wtf : idtoeqv f-path ≡ idtoeqv refl
+        -- wtf : idtoeqv f-path ≡ idtoeqv refl
-        wtf = ap idtoeqv helper
+        -- wtf = ap idtoeqv helper
       in {!   !}
 
     lol : true ≡ false