remove existing stuff

src/LogRel.agda

@@ -1,202 +0,0 @@
--- https://www.cs.uoregon.edu/research/summerschool/summer24/lectures/Ahmed.pdf
-
-module LogRel where
-
-open import Data.Bool
-open import Data.String
-open import Data.Sum
-open import Data.Empty
-open import Data.Nat
-open import Data.Maybe
-open import Data.Product
-open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Negation
-open import Relation.Nullary using (Dec; yes; no)
-
-_∙_ = trans
-
-data type : Set where
-  bool : type
-  _-→_ : type → type → type
-
-data term : Set where
-  `_ : String → term
-  true : term
-  false : term
-  `if_then_else_ : term → term → term → term
-  `λ[_∶_]_ : String → type → term → term
-  _`∙_ : term → term → term
-
-replace : (e : term) → (x : String) → (v : term) → term
-replace (` y) x v = if x == y then v else (` y)
-replace true x v = true
-replace false x v = false
-replace (`if e then e₁ else e₂) x v = `if (replace e x v) then replace e₁ x v else replace e₂ x v
-replace e @ (`λ[ y ∶ t ] e′) x v = if x == y then e else (`λ[ y ∶ t ] replace e′ x v)
-replace (e₁ `∙ e₂) x v = replace e₁ x v `∙ replace e₂ x v
-
-data value : term → Set where
-  true : value true
-  false : value false
-  `λ[_∶_]_ : (x : String) → (t : type) → (e : term) → value (`λ[ x ∶ t ] e)
-
-to-value : (t : term) → Maybe (value t)
-to-value (` x) = nothing
-to-value true = just true
-to-value false = just false
-to-value (`if t then t₁ else t₂) = nothing
-to-value (`λ[ x ∶ t ] e) = just (`λ[ x ∶ t ] e)
-to-value (t `∙ t₁) = nothing
-
-is-value : (t : term) → Set
-is-value t = Is-just (to-value t)
-
-data ectx : Set where
-  [∙] : ectx
-  `if_then_else_ : ectx → term → term → ectx
-  _`∙_ : ectx → term → ectx
-  _∙`_ : {e : term} → value e → ectx → ectx
-
-data ctx : Set where
-  ∅ : ctx
-  _,_∶_ : ctx → String → type → ctx
-
-data sub : Set where
-  ∅ : sub
-  _,_≔_ : sub → String → term → sub
-
-evalsub : sub → term → term
-evalsub ∅ e = e
-evalsub (γ , x ≔ v) e = replace (evalsub γ e) x v
-
-lookup : ctx → String → Maybe type
-lookup ∅ x = nothing
-lookup (Γ , y ∶ t) x = if (x == y) then just t else lookup Γ x
-
--- Some dumb stuff
-
-lemma1 : ∀ (γ : sub) → evalsub γ true ≡ true
-lemma1 ∅ = refl
-lemma1 (γ , x ≔ v) = cong (λ z → replace z x v) (lemma1 γ)
-
-lemma2 : ∀ (γ : sub) → evalsub γ false ≡ false
-lemma2 ∅ = refl
-lemma2 (γ , x ≔ v) = cong (λ z → replace z x v) (lemma2 γ)
-
--- Operational semantics
-
-data _↦_ : term → term → Set where
-  rule1 : (e1 e2 : term) → (if true then e1 else e2) ↦ e1
-  rule2 : (e1 e2 : term) → (if false then e1 else e2) ↦ e2
-  rule3 : (x : String) → (t : type) → (e : term) → (v : term)
-    → ((`λ[ x ∶ t ] e) `∙ v) ↦ replace e x v
-
-data iter : ℕ → term → term → Set where
-  iter-zero : ∀ (e : term) → iter zero e e
-  iter-suc : ∀ (n : ℕ) → (e e′ e′′ : term) → iter n e e′ → (e′ ↦ e′′) → iter (suc n) e′ e′′
-
-_↦∙_ : term → term → Set
-e ↦∙ e′ = Σ ℕ λ n → iter n e e′
-
--- Type judgments
-
-data _⊢_∶_ : ctx → term → type → Set where
-  type1 : (Γ : ctx) → Γ ⊢ true ∶ bool
-  type2 : (Γ : ctx) → Γ ⊢ false ∶ bool
-  type3 : (Γ : ctx) → (x : String) → (tw : Is-just (lookup Γ x)) → Γ ⊢ ` x ∶ to-witness tw
-  type4 : (Γ : ctx) → (x : String) → (e : term) → (t₁ t₂ : type)
-    → ((Γ , x ∶ t₁) ⊢ e ∶ t₂) → Γ ⊢ `λ[ x ∶ t₁ ] e ∶ (t₁ -→ t₂)
-  type5 : (Γ : ctx) → (e₁ e₂ : term) → (t t₂ : type)
-    → (Γ ⊢ e₁ ∶ (t₂ -→ t)) → (Γ ⊢ e₂ ∶ t₂) → Γ ⊢ e₁ `∙ e₂ ∶ t
-  type6 : (Γ : ctx) → (e e₁ e₂ : term) → (t : type)
-    → (Γ ⊢ e ∶ bool) → (Γ ⊢ e₁ ∶ t) → (Γ ⊢ e₂ ∶ t)
-    → Γ ⊢ `if e then e₁ else e₂ ∶ t
-
--- Type soundness
-
-type-soundness : ∀ {e e′ t} → (∅ ⊢ e ∶ t) → (e ↦∙ e′) → Set
-type-soundness {e = e} {e′ = e′} {t = t} prf eval =
-  (value e) ⊎ Σ term λ e′′ → e′ ↦ e′′
-
--- Safety
-
-safe : term → Set
-safe e = ∀ (e′ : term) → e ↦∙ e′ → (value e′) ⊎ Σ term (λ e′′ → (e′ ↦ e′′))
-
--- Logical relations
-
-data V : type → term → Set
-data E : type → term → Set
-  
-data V where
-  bool-true : V bool true
-  bool-false : V bool false
-  →-λ : ∀ (x : String) → (e : term) → (t₁ t₂ : type)
-    → ((v : term) → V t₁ v → E t₂ (replace e x v)) → V (t₁ -→ t₂) (`λ[ x ∶ t₁ ] e)
-
-irred : (e : term) → Set
-irred e = ¬ (Σ term (λ e′ → e ↦ e′))
-
-data E where
-  erel : ∀ (e : term) → (t : type)
-    → ((e′ : term) → ((e ↦∙ e′) × irred e′) → V t e′) → E t e
-
-data G : ctx → sub → Set where
-  nil : G ∅ ∅
-  cons : ∀ (Γ : ctx) → (x : String) → (t : type) → (γ : sub) → (v : term)
-    → (G Γ γ) ⊎ V t v
-    → G (Γ , x ∶ t) (γ , x ≔ v)
-
--- Semantically well-typed
-
-_⊨_∶_ : (Γ : ctx) → (e : term) → (t : type) → Set 
-Γ ⊨ e ∶ t = ∀ (γ : sub) → G Γ γ → E t (evalsub γ e)
-
--- Theorem 4.2: fundamental property of logical relations
-
-theorem42 : ∀ (Γ : ctx) → (e : term) → (t : type) → Γ ⊢ e ∶ t → Γ ⊨ e ∶ t
-theorem42 Γ e t (type1 .Γ) γ G[γ] =
-  subst (E bool) (sym (lemma1 γ)) (erel e bool helper) where
-    helper : (e′ : term) → (true ↦∙ e′) × irred e′ → V bool e′
-    helper e′ ((zero , iter-zero .true) , snd) = bool-true
-    helper e′ ((suc n , iter-suc .n e .true .true fst (rule1 .true e2)) , snd) = bool-true
-    helper e′ ((suc n , iter-suc .n e .true .true fst (rule2 e1 .true)) , snd) = bool-true
-theorem42 Γ e t (type2 .Γ) γ G[γ] =
-  subst (E bool) (sym (lemma2 γ)) (erel e bool helper) where
-    helper : (e′ : term) → (false ↦∙ e′) × irred e′ → V bool e′
-    helper e′ ((zero , iter-zero .false) , snd) = bool-false
-    helper e′ ((suc n , iter-suc .n e .false .false fst (rule1 .false e2)) , snd) = bool-false
-    helper e′ ((suc n , iter-suc .n e .false .false fst (rule2 e1 .false)) , snd) = bool-false
-theorem42 Γ e t (type3 .Γ x tw) γ G[γ] = erel {!   !} {!   !} {!   !}
-theorem42 Γ e t (type4 .Γ x e₁ t₁ t₂ sts) ∅ G[γ] = erel (`λ[ x ∶ t₁ ] e₁) t helper where
-  helper : (e′ : term) → ((`λ[ x ∶ t₁ ] e₁) ↦∙ e′) × irred e′ → V (t₁ -→ t₂) e′
-  helper e′ ((zero , iter-zero .(`λ[ x ∶ t₁ ] e₁)) , snd) =
-    →-λ x e₁ t₁ t₂ λ v x₁ → erel {!   !} {!   !} {!   !}
-  helper e′ ((suc n , fst) , snd) = {!   !}
-theorem42 Γ e t (type4 .Γ x e₁ t₁ t₂ sts) (γ , x₁ ≔ x₂) G[γ] =
-  {!   !}
-theorem42 Γ e t (type5 .Γ e₁ e₂ .t t₂ sts sts₁) = {!   !}
-theorem42 Γ e t (type6 .Γ e₁ e₂ e₃ .t sts sts₁ sts₂) ∅ G[γ] =
-  erel (`if e₁ then e₂ else e₃) t helper where
-    helper : (e′ : term) → ((`if e₁ then e₂ else e₃) ↦∙ e′) × irred e′ → V t e′
-    helper e′ ((zero , iter-zero .(`if e₁ then e₂ else e₃)) , snd) =
-      ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) 
-    helper e′ ((suc n , iter-suc .n e .(`if e₁ then e₂ else e₃) .(`if e₁ then e₂ else e₃) fst (rule1 .(`if e₁ then e₂ else e₃) e2)) , snd) =
-      ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) 
-    helper e′ ((suc n , iter-suc .n e .(`if e₁ then e₂ else e₃) .(`if e₁ then e₂ else e₃) fst (rule2 e1 .(`if e₁ then e₂ else e₃))) , snd) =
-      ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) 
-theorem42 Γ e t (type6 .(Γ₁ , x ∶ t₁) e₁ e₂ e₃ .t sts sts₁ sts₂) (γ , x ≔ x₁) (cons Γ₁ .x t₁ .γ .x₁ (inj₁ x₂)) = {!   !}
-theorem42 Γ e t (type6 .(Γ₁ , x ∶ t₁) e₁ e₂ e₃ .t sts sts₁ sts₂) (γ , x ≔ x₁) (cons Γ₁ .x t₁ .γ .x₁ (inj₂ y)) = {!   !}
-
--- Theorem 4.1: semantic type soundness
-
-theorem41 : ∀ (e : term) → (t : type) → (∅ ⊢ e ∶ t) → safe e
-theorem41 e t ts = goal1 where
-  swt : ∅ ⊨ e ∶ t
-  swt = theorem42 ∅ e t ts
- 
-  goal2 : E t e
-  goal2 = swt ∅ nil
-
-  goal1 : safe e         
-  goal1 e′ prf = {!   !} 

src/VanDoornDissertation/HoTT/LongExactSequence.agda

@@ -1,4 +0,0 @@
-{-# OPTIONS --cubical --safe #-}
-
-module VanDoornDissertation.HoTT.LongExactSequence where
-

src/VanDoornDissertation/PropTrunc.agda

@@ -1,26 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module VanDoornDissertation.PropTrunc where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Equiv
-open import Cubical.HITs.Truncation
-open import Cubical.HITs.PropositionalTruncation
-
--- Theorem 3.1.8. The map A 7 → {A}∞ satisfies all the properties of the propositional
--- truncation ‖−‖, including the universe level and judgmental computation rule on point
--- constructors.
-
-ptrunc-equiv-trunc : {A : Type} → ∥ A ∥₁ ≃ (∥ A ∥ 1)
-ptrunc-equiv-trunc {A} = f , record { equiv-proof = eqv } where
-  f : ∥ A ∥₁ → (∥ A ∥ 1)
-  f ∣ x ∣₁ = ∣ x ∣ 
-  f (squash₁ x y i) = {!   !}
-
-  g : ∥ A ∥ 1 → ∥ A ∥₁
-  g ∣ x ∣ = ∣ x ∣₁
-  g (hub f₁) = {!   !}
-  g (spoke f₁ x i) = {!   !}
- 
-  eqv : (y : ∥ A ∥ 1) → isContr (fiber f y)
-  eqv y = {!   !} , {!   !}

src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda

@@ -1,7 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module VanDoornDissertation.Spectral.Algebra.SpectralSequence where
-
-open import Cubical.Foundations.Prelude
-
-record convergent-spectral-sequence : Type where