wip

src/VanDoornDissertation/PropTrunc.agda

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

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