auto gitdoc commit

README.md

@@ -1,8 +1,8 @@
-cubical
+type-theory
 ===
 
-This repository tracks my exploration into cubical type theory, including my
-progress into research for my master's degree.
+This repository tracks my exploration into HoTT and cubical type theory,
+including my progress into research for my master's degree.
 
 Links:
 

src/HottBook/Chapter2.lagda.md

@@ -87,26 +87,25 @@ apd {l₁} {l₂} {A} {P} {x} {y} f p =
 TODO
 
 ```
-transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A} (B : Set l₂) → (p : x ≡ y) → (b : B)
+transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
+  → (B : Set l₂)
+  → (p : x ≡ y)
+  → (b : B)
   → transport (λ _ → B) p b ≡ b
-transportconst {l₁} {l₂} {A} {x} B p b =
-  let
-    D : (x y : A) → (p : x ≡ y) → Set l₂
-    D x y p = transport (λ _ → B) p b ≡ b
-
-    d : (x : A) → D x x refl
-    d x = refl
-  in
-  J (λ x p → transport (λ _ → B) p b ≡ b) p (d x)
+transportconst {l₁} {l₂} {A} {x} {y} B p b =
+  J (λ x y p → transport (λ _ → B) p b ≡ b) (λ x → refl) x y p
 ```
 
 ### Lemma 2.3.8
 
 ```
--- lemma238 : {A B : Set} (f : A → B) {x y : A} (p : x ≡ y)
---   → apd f p ≡ transportconst B p (f x) ∙ ap f p
--- lemma238 {A} {B} f {x} p =
---   J (λ y p → apd f p ≡ transportconst B p (f x) ∙ ap f p) p refl
+lemma238 : {l : Level} {A B : Set l}
+  → (f : A → B) 
+  → {x y : A} 
+  → (p : x ≡ y)
+  → apd f p ≡ transportconst B p (f x) ∙ ap f p
+lemma238 {l} {A} {B} f {x} {y} p =
+  J (λ x y p → apd f p ≡ transportconst B p (f x) ∙ ap f p) (λ x → refl) x y p
 ```
 
 ### Lemma 2.3.9