auto gitdoc commit

src/HottBook/Chapter2.lagda.md

@@ -243,7 +243,7 @@ qinv-to-isequiv q = record
   { g = qinv.g q
   ; g-id = qinv.α q
   ; h = qinv.g q
-  ; h-id = {! qinv.β q  !}
+  ; h-id = qinv.β q
   }
 ```
 
@@ -308,44 +308,44 @@ postulate
 ### Lemma 2.10.1
 
 ```
-idToEquiv : {A B : Set}
-  → (A ≡ B)
-  → A ≃ B
-idToEquiv {A} {B} p = func , equiv
-  where
-    func : A → B
-    func a = transport id p a
+-- idToEquiv : {A B : Set}
+--   → (A ≡ B)
+--   → A ≃ B
+-- idToEquiv {A} {B} p = func , equiv
+--   where
+--     func : A → B
+--     func a = transport id p a
 
-    func-inv : B → A
-    func-inv b = transport id (sym p) b
+--     func-inv : B → A
+--     func-inv b = transport id (sym p) b
 
-    p* : A → B
-    p* = transport id p
+--     p* : A → B
+--     p* = transport id p
 
-    wtf3 : A → A
-    wtf3 = J (λ A' B' p' → A → A') (λ A' → {! id  !}) A B p
+--     wtf3 : A → A
+--     wtf3 = J (λ A' B' p' → A → A') (λ A' → {! id  !}) A B p
 
-    wtf3-is-id : wtf3 ∼ id
-    wtf3-is-id x = {!  !}
+--     wtf3-is-id : wtf3 ∼ id
+--     wtf3-is-id x = {!  !}
 
-    wtf3-qinv : qinv wtf3
-    wtf3-qinv = record
-      { g = wtf3
-      ; α = λ x → {!   !}
-      ; β = λ x → {!   !}
-      }
+--     wtf3-qinv : qinv wtf3
+--     wtf3-qinv = record
+--       { g = wtf3
+--       ; α = λ x → {!   !}
+--       ; β = λ x → {!   !}
+--       }
 
-    -- homotopy : (func ∘ func-inv) ∼ id
-    -- homotopy x = 
-    --   let
-    --   in {!    !}
+--     -- homotopy : (func ∘ func-inv) ∼ id
+--     -- homotopy x = 
+--     --   let
+--     --   in {!    !}
 
-    equiv = record
-      { g = func-inv
-      ; g-id = {!   !}
-      ; h = func-inv
-      ; h-id = {!   !}
-      }
+--     equiv = record
+--       { g = func-inv
+--       ; g-id = {!   !}
+--       ; h = func-inv
+--       ; h-id = {!   !}
+--       }
 ```
 
 ### Axiom 2.10.3 (Univalence)

src/HottBook/Chapter3.lagda.md

@@ -1,9 +1,6 @@
 ```
 module HottBook.Chapter3 where
 
-open import Relation.Binary.PropositionalEquality
-open import Data.Sum
-open import Data.Empty
 open import HottBook.Chapter1
 
 ```
@@ -13,7 +10,7 @@ open import HottBook.Chapter1
 ### Definition 3.1.1
 
 ```
-isSet : (A : Type) → Type
+isSet : (A : Set) → Set
 isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ```
 
@@ -26,22 +23,22 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 #### i. Decidability of types
 
 ```
-decidable : (A : Type) → Type
-decidable A = A ⊎ ¬ A
+-- decidable : (A : Set) → Set
+-- decidable A = A ⊎ ¬ A
 ```
 
 #### ii. Decidability of type families
 
 ```
-dep-decidable : {A : Type} → (B : A → Type) → Type
-dep-decidable {A} B = (a : A) → (B a ⊎ ¬ B a)
+-- dep-decidable : {A : Set} → (B : A → Set) → Set
+-- dep-decidable {A} B = (a : A) → (B a ⊎ ¬ B a)
 ```
 
 #### iii. Decidable equality
 
 ```
-decidable-equality : (A : Type) → Type
-decidable-equality A = (a b : A) → (a ≡ b) ⊎ ¬ (a ≡ b)
+-- decidable-equality : (A : Set) → Set
+-- decidable-equality A = (a b : A) → (a ≡ b) ⊎ ¬ (a ≡ b)
 ```
 
 So I think the interesting property about this is that normally a function f
@@ -61,20 +58,20 @@ paths for a ≡ b.
 > any type with decidable equality is a set.
 
 ```
-decidable-equality-is-set : (A : Type) → decidable-equality A → isSet A
-decidable-equality-is-set A f x y p q =
-  let
-    res = f x y
+-- decidable-equality-is-set : (A : Set) → decidable-equality A → isSet A
+-- decidable-equality-is-set A f x y p q =
+--   let
+--     res = f x y
 
-    -- We can eliminate the bottom case because if p and q exist, it must be inj₁
-    center : x ≡ y
-    center = [ (λ p′ → p′) , (λ p′ → ⊥-elim (p′ _)) ] (f x y)
+--     -- We can eliminate the bottom case because if p and q exist, it must be inj₁
+--     center : x ≡ y
+--     center = [ (λ p′ → p′) , (λ p′ → ⊥-elim (p′ _)) ] (f x y)
 
-    -- What i want is: given any path x ≡ y, prove that it equals this inj₁ (res f x y)
-    guarantee : (p′ : x ≡ y) → center ≡ p′
-    guarantee p′ = J (λ the what → the ≡ p′) ? ?
+--     -- What i want is: given any path x ≡ y, prove that it equals this inj₁ (res f x y)
+--     guarantee : (p′ : x ≡ y) → center ≡ p′
+--     guarantee p′ = J (λ the what → the ≡ p′) ? ?
 
-    info = ?
-  in
-  J (λ the what → p ≡ ?) refl ?
+--     info = ?
+--   in
+--   J (λ the what → p ≡ ?) refl ?
 ```