wtf

.gitignore

@@ -4,4 +4,5 @@ node_modules
 
 logseq
 !logseq/custom.edn
-!logseq/custom.css
+!logseq/custom.css
+.pijul

.ignore

@@ -0,0 +1,2 @@
+.git
+.DS_Store

src/CubicalHott/Chapter2.agda

@@ -17,7 +17,9 @@ module lemma211 where
 
 module lemma212 where
   lemma : {A : Type l} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
-  lemma {x = x} p q i = hcomp (λ j → λ { (i = i0) → x ; (i = i1) → q j }) (p i)
+  lemma {x = x} p q i = hcomp
+    (λ j → λ { (i = i0) → x ; (i = i1) → q j })
+    (p i)
 
 module lemma214 where
   private

src/CubicalHottBook/Chapter2.lagda.md

@@ -1,92 +0,0 @@
-```
-{-# 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 (λ _ → B) p b ≡ b
-transportconst B p b i = {!   !}
-```
-
-### 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
-
-  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

@@ -1,38 +0,0 @@
-```
-{-# 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

@@ -1,12 +0,0 @@
-{-# 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.Foundations.Equiv public
-
-module Inductive where
-  open import Cubical.Data.Equality public
-
-open Inductive public using (id)