From 196eeec6e24e1b8d4f0a0b21b4e6ea46a7f62125 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 15 Oct 2024 23:13:53 -0500
Subject: [PATCH] step 1

---
 src/ThesisWork/Pi3S2/Step1.agda | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 src/ThesisWork/Pi3S2/Step1.agda

diff --git a/src/ThesisWork/Pi3S2/Step1.agda b/src/ThesisWork/Pi3S2/Step1.agda
new file mode 100644
index 0000000..c5f2f58
--- /dev/null
+++ b/src/ThesisWork/Pi3S2/Step1.agda
@@ -0,0 +1,18 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Pi3S2.Step1 where
+
+open import Agda.Primitive
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Homotopy.Loopspace
+
+arrow∙ : {l : Level} → Type (lsuc l)
+arrow∙ {l} = Σ (Pointed l) (λ X → Σ (Pointed l) (λ Y → X →∙ Y))
+
+F : {l : Level} → arrow∙ {l} → arrow∙ {l}
+F x @ (X , Y , f) = {! fiber   !} , X , {!  fst !}
\ No newline at end of file