cubical stuff

src/CubicalHottBook/Chapter2.lagda.md

@@ -0,0 +1,93 @@
+```
+{-# OPTIONS --cubical --without-K #-}
+module CubicalHottBook.Chapter2 where
+
+open import CubicalHottBook.Prelude
+
+private
+  variable
+    l l2 : Level
+```
+
+### Lemma 2.3.5
+
+```
+transportconst : {A : Type l} {x y : A}
+  → (B : Type l2)
+  → (p : x ≡ y)
+  → (b : B)
+  → subst ? p ? ≡ ?
+transportconst B p b = ?
+```
+
+### Definition 2.4.1
+
+```
+_∼_ : {X : Type l} {Y : X → Type l2} → (f g : (x : X) → Y x) → Type (ℓ-max l l2)
+_∼_ {X = X} f g = (x : X) → f x ≡ g x
+```
+
+### Definition 2.4.6
+
+```
+record qinv {A B : Type} (f : A → B) : Type where
+  constructor mkQinv
+  field
+    g : B → A
+    forward : (f ∘ g) ∼ id
+    backward : (g ∘ f) ∼ id
+```
+
+### Example 2.4.7
+
+```
+id-qinv : {A : Type} → qinv (id {A = A})
+id-qinv {A = A} = mkQinv id id-homotopy id-homotopy where
+  id-homotopy : (x : A) → (id ∘ id) x ≡ id x
+  id-homotopy x = refl
+```
+
+### Definition 2.4.10
+
+```
+mkIsEquiv : {A B : Type} {f : A → B}
+  → (g : B → A)
+  → (f ∘ g) ∼ id
+  → (g ∘ f) ∼ id
+  → isEquiv f
+mkIsEquiv {B = B} {f = f} g forward backward = record { equiv-proof = eqv-prf } where
+  postulate
+    helper : (y : B) → (z : fiber f y) → (g y , forward y) ≡ z
+  -- helper y (x , p) = Σ-≡,≡→≡ (ap g (sym p) ∙ backward x , {!  !})
+
+  eqv-prf : (y : B) → isContr (fiber f y) 
+  eqv-prf y = (g y , forward y) , helper y
+```
+
+### Theorem 2.11.3
+
+```
+theorem2∙11∙3 : {A B : Type} {f g : A → B} {a a' : A}
+  → (p : a ≡ a')
+  → (q : f a ≡ g a)
+  → subst (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ ap g p
+theorem2∙11∙3 refl q = sym (unitR q)
+```
+
+### Theorem 2.11.5
+
+```
+postulate
+  theorem2∙11∙5 : {A : Type} {a a' : A}
+    → (p : a ≡ a')
+    → (q : a ≡ a)
+    → (r : a' ≡ a')
+    → (transport (λ x → x ≡ x) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
+-- theorem2∙11∙5 {a = a} refl q r = f , mkIsEquiv g {!   !} {!   !} where
+--   f : (q ≡ r) → (q ∙ refl ≡ r)
+--   f refl = unitR q
+--   g : (q ∙ refl ≡ r) → (q ≡ r)
+--   g refl = sym (unitR q)
+--   forward : (f ∘ g) ∼ id
+--   forward refl = {! refl  !}
+```

src/CubicalHottBook/Chapter6.lagda.md

@@ -0,0 +1,38 @@
+```
+{-# OPTIONS --cubical --without-K #-}
+module CubicalHottBook.Chapter6 where
+
+open import CubicalHottBook.Prelude
+open import CubicalHottBook.Chapter2
+```
+
+```
+dep-path : {l l2 : Level} {A : Set l} {x y : A} → (P : A → Set l2) → (p : x ≡ y) → (u : P x) → (v : P y) → Set l2
+dep-path P p u v = transport P p u ≡ v
+
+syntax dep-path P p u v = u ≡[ P , p ] v
+```
+
+## Circle
+
+### Lemma 6.2.5
+
+```
+lemma6∙2∙5 : {A : Type}
+  → (a : A)
+  → (p : a ≡ a)
+  → S¹ → A
+lemma6∙2∙5 a p base = a
+lemma6∙2∙5 a p (S¹.loop i) = {!   !}
+```
+
+### Lemma 6.2.8
+
+```
+lemma6∙2∙8 : {A : Type} {f g : S¹ → A}
+  → (p : f base ≡ g base)
+  → (q : (ap f loop) ≡[ (λ x → x ≡ x) , p ] (ap g loop))
+  → (x : S¹) → f x ≡ g x
+lemma6∙2∙8 p q base = p
+lemma6∙2∙8 p q (S¹.loop i) = {!    !}
+```

src/CubicalHottBook/Prelude.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --cubical --without-K #-}
+module CubicalHottBook.Prelude where
+
+open import Cubical.Foundations.Function public
+open import Data.Product.Properties public
+open import Cubical.Foundations.Prelude public
+open import Cubical.Data.Equality public using (id)
+open import Cubical.Foundations.Equiv public
+