From abde273e80e9e7ac1c921fafec9f8f0be32cd6d4 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 22 Apr 2024 01:44:06 +0000 Subject: [PATCH] auto gitdoc commit --- README.md | 6 +++--- src/HottBook/Chapter2.lagda.md | 27 +++++++++++++-------------- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/README.md b/README.md index 0fc0199..e872aa4 100644 --- a/README.md +++ b/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: diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 9498d82..907a6b4 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/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