LES definition similar to the one used by Floris, closes #25

src/HomotopyTheory/LES.agda

@@ -0,0 +1,93 @@
+{-# OPTIONS --cubical #-}
+
+module HomotopyTheory.LES where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Equiv
+open import Data.Nat
+open import Data.Fin
+open import Data.Product
+open import Cubical.Homotopy.Base
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Base
+open import Cubical.Homotopy.Group.LES
+open import Cubical.HITs.SetTruncation renaming (map to mapTrunc)
+open import Cubical.HITs.SetTruncation.Fibers
+
+private
+  variable
+    X Y : Type
+
+LES-node : ∀ {l} → {X Y : Pointed l} → (f : X →∙ Y) → ℕ × Fin 3 → Type l
+LES-node {Y = Y} f (n , zero) = π n Y
+LES-node {X = X} f (n , suc zero) = π n X
+LES-node {X = (X , x)} {Y = (Y , y)} (f , f-eq) (n , suc (suc zero)) =
+    let F = fiber f y in
+    π n (F , x , f-eq)
+
+sucF : ℕ × Fin 3 → ℕ × Fin 3
+sucF (n , zero) = n , suc zero
+sucF (n , suc zero) = n , suc (suc zero)
+sucF (n , suc (suc zero)) = suc n , zero
+
+LES-edge : ∀ {l} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → (n : ℕ × Fin 3)
+    → LES-node f∙ (sucF n) → LES-node f∙ n
+LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , zero) = h n where
+    h1 : ∀ (n : ℕ) → (Ω^ n) X∙ →∙ (Ω^ n) Y∙
+    h1 zero = f∙
+    h1 (suc n) = (λ x → refl) , helper where
+        helper : refl ≡ snd (Ω ((Ω^ n) Y∙))
+        helper i j = (Ω^ n) (Y , y) .snd
+
+        -- helper = λ i j →
+        --     let
+        --         top : (Ω^ n) (Y , y) .fst
+        --         top = {!  refl !}
+        --         u = λ k → λ where
+        --             (i = i0) → {!   !}
+        --             (i = i1) → {!   !}
+        --             (j = i0) → {!   !}
+        --             (j = i1) → {!   !}
+        --     in hcomp u {!   !}
+
+    h : ∀ (n : ℕ) → π n X∙ → π n Y∙
+    h n = mapTrunc (fst (h1 n))
+
+    -- h zero ∣ a ∣₂ = ∣ f a ∣₂
+    -- h (suc n) ∣ a ∣₂ = let IH = h n ∣ a i0 ∣₂ in ∣ {!   !} ∣₂
+    -- h zero (squash₂ a b p q i j) = squash₂ (h 0 a) (h 0 b) (cong (h 0) p) (cong (h 0) q) i j
+    -- h (suc n) (squash₂ a b p q i j) = {!   !}
+
+LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc zero) = h n where
+    F = fiber f y
+    
+    h1 : ∀ (n : ℕ) → (Ω^ n) (F , x , f-eq) →∙ (Ω^ n) X∙
+    h1 zero = fst , refl
+    h1 (suc n) = (λ f i → (Ω^ n) (X , x) .snd) , λ i j → (Ω^ n) (X , x) .snd
+
+    h : ∀ (n : ℕ) → π n (F , x , f-eq) → π n X∙
+    h n = mapTrunc (fst (h1 n))
+
+LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc (suc zero)) = h n where
+    F = fiber f y
+
+    h1 : ∀ (n : ℕ) → (Ω^ (suc n)) Y∙ →∙ (Ω^ n) (F , x , f-eq)
+    h1 zero = (λ y → x , f-eq) , refl
+    h1 (suc n) = (λ y i → (Ω^ n) (F , x , f-eq) .snd) , λ i j → (Ω^ n) (F , x , f-eq) .snd
+
+    h : ∀ (n : ℕ) → π (suc n) Y∙ → π n (F , x , f-eq)
+    h n = mapTrunc (fst (h1 n))
+
+-- LES-edge f n_ with mapN n_
+-- LES-edge {X = X∙ @ (X , x)} {Y = Y∙ @ (Y , y)} f n_ | (n , zero) = {! h  !} where
+--     h : π n X∙ → π n Y∙
+--     h ∣ x ∣₂ = ∣ {!   !} ∣₂
+--     h (squash₂ z z₁ p q i i₁) = {!   !}
+--     -- z : LES-node f (mapN (suc n_))
+--     -- z : π n X
+--     -- z : ∥ typ ((Ω^ 0) X) ∥₂
+--     -- z : ∥ typ X ∥₂
+--     -- z : ∥ typ X ∥₂
+-- LES-edge f n_ | (n , suc zero) = λ z → {!   !}       
+-- LES-edge f n_ | (n , suc (suc zero)) = λ z → {!   !} 

src/LogRel.agda

@@ -1,3 +1,5 @@
+-- https://www.cs.uoregon.edu/research/summerschool/summer24/lectures/Ahmed.pdf
+
 module LogRel where
 
 open import Data.Bool