step 1

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 !}