From 040a68bc2a1bb4cd26ebdf79ac8b8e3abc7d8310 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 9 Aug 2024 04:55:32 -0500
Subject: [PATCH] wip

---
 src/VanDoornDissertation/PropTrunc.agda       | 26 +++++++++++++++++++
 .../Spectral/Algebra/SpectralSequence.agda    |  7 +++++
 2 files changed, 33 insertions(+)
 create mode 100644 src/VanDoornDissertation/PropTrunc.agda
 create mode 100644 src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda

diff --git a/src/VanDoornDissertation/PropTrunc.agda b/src/VanDoornDissertation/PropTrunc.agda
new file mode 100644
index 0000000..55bdba9
--- /dev/null
+++ b/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 = {!   !} , {!   !}
\ No newline at end of file
diff --git a/src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda b/src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda
new file mode 100644
index 0000000..8f7d31c
--- /dev/null
+++ b/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
\ No newline at end of file