remove existing

src/VanDoornDissertation/HIT.lagda.md

@@ -1,31 +0,0 @@
-```
-module VanDoornDissertation.HIT where
-
-open import HottBook.Chapter1
-```
-
-# 3 Higher Inductive Types
-
-## 3.1 Propositional Truncation
-
-```
-postulate
-  one-step-truncation : Set → Set
-  f : {A : Set} → A → one-step-truncation A
-  e : {A : Set} → (x y : A) → f x ≡ f y
--- data one-step-truncation (A : Set) : Set where
---   f : A → one-step-truncation A
---   e : (x y : A) → f x ≡ f y
-
-weakly-constant : {A B : Set} → (g : A → B) → Set
-weakly-constant {A} g = {x y : A} → g x ≡ g y
-
-definition3∙1∙1 : {A : Set} → one-step-truncation A → ℕ → Set
-definition3∙1∙1 {A} trunc zero = A
-definition3∙1∙1 {A} trunc (suc n) = one-step-truncation (definition3∙1∙1 trunc n)
-
-fs : {A : Set} → one-step-truncation A → (n : ℕ) → Set
-fs trunc n = (definition3∙1∙1 trunc n) → (definition3∙1∙1 trunc (suc n))
-
--- lemma3∙1∙3 : {X : Set} → {x : X} → is
-```

src/VanDoornDissertation/HoTT/Sphere2.agda

@@ -1,3 +0,0 @@
-{-# OPTIONS --cubical #-}
-module VanDoornDissertation.HoTT.Sphere2 where
-

src/VanDoornDissertation/Preliminaries.lagda.md

@@ -1,93 +0,0 @@
-```
-{-# OPTIONS --cubical --no-load-primitives #-}
-module VanDoornDissertation.Preliminaries where
-
-open import CubicalHott.Chapter1
-open import CubicalHott.Chapter2
-```
-
-### 2.2.1 Paths
-
-```
-```
-
-### 2.2.3 More on paths
-
-#### Pathovers
-
-```
-dependent-path : {A : Type} 
-  → (P : A → Type) 
-  → {x y : A} 
-  → (p : x ≡ y)
-  → (u : P x) → (v : P y) → Type
-dependent-path P p u v = transport P p u ≡ v
-
-syntax dependent-path P p u v = u ≡[ P , p ] v
-
--- https://git.mzhang.io/school/type-theory/issues/16
-apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b}
-    → (f : (i : I) → (a : A i) → B i a)
-    → {x : A i0}
-    → {y : A i1}
-    → (p : PathP A x y)
-    → PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
-apd f p i = f i (p i)
-```
-
-#### Squares
-
-```
-Square : {A : Type} {a00 a10 a01 a11 : A}
-  → (p : a00 ≡ a01)
-  → (q : a00 ≡ a10)
-  → (s : a01 ≡ a11)
-  → (r : a10 ≡ a11)
-  → Type
-Square p q s r = PathP (λ i → p i ≡ r i) q s
-```
-
-#### Squareovers and cubes
-
-```
-
-```
-
-#### Paths in type formers
-
-```
-
-```
-
-### 2.2.5 Pointed Types
-
-#### Definition 2.2.6
-
-```
-data pointed (A : Type) : Type where
-  mkPointed : (a₀ : A) → pointed A
-
-1-is-pointed : pointed 𝟙
-1-is-pointed = mkPointed tt
-
-2-is-pointed : pointed 𝟚
-2-is-pointed = mkPointed false
-
-S⁰ = 2-is-pointed
-
-_×_-is-pointed : {A B : Type} → pointed A → pointed B → pointed (A × B)
-_×_-is-pointed {A} {B} (mkPointed a₀) (mkPointed b₀) = mkPointed (a₀ , b₀)
-```
-
-### 2.2.6 Higher inductive types
-
-```
-data Interval : Type where
-  0I : Interval
-  1I : Interval
-  seg : 0I ≡ 1I
-
-data Quotient (A : Type) (R : A → A → Type) : Type where
-  x : A → Quotient A R
-  glue : (a a' : A) → R a a' → x a ≡ x a'
-```

src/VanDoornDissertation/Spectral/README.md

@@ -1 +0,0 @@
-This is an attempt at doing a direct translation.