Skip to content

Commit

Permalink
w
Browse files Browse the repository at this point in the history
  • Loading branch information
@aljungstrom
aljungstrom committed Jun 8, 2023
1 parent 52429ff commit ea75092
Show file tree
Hide file tree
Showing 3 changed files with 0 additions and 549 deletions.
209 changes: 0 additions & 209 deletions Cubical/HITs/Join/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -482,212 +482,3 @@ fst joinAnnihilL = inl tt*
snd joinAnnihilL (inl tt*) = refl
snd joinAnnihilL (inr a) = push tt* a
snd joinAnnihilL (push tt* a i) j = push tt* a (i ∧ j)

open import Cubical.Foundations.Pointed
open import Cubical.Homotopy.Loopspace

module _ {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
fib⋆ : Pointed _
proj₁ fib⋆ = fiber (fst f) (pt B)
snd fib⋆ = (pt A) , (snd f)

fib-gen : (b : fst B) → Type _
fib-gen b = fiber (fst f) b

fib-proj : fib⋆ →∙ A
proj₁ fib-proj = fst
snd fib-proj = refl

fib-cofib : Type _
fib-cofib = cofib (fst fib-proj)

GaneaMap : fib-cofib → fst B
GaneaMap (inl x) = pt B
GaneaMap (inr x) = fst f x
GaneaMap (push a i) = a .snd (~ i)

GaneaMap* : (b : fst B) (f : A →∙ (fst B , b)) → cofib {A = fiber (fst f) b} {B = fst A} fst → fst B
GaneaMap* b f (inl x) = b
GaneaMap* b f (inr x) = fst f x
GaneaMap* b f (push a i) = a .snd (~ i)

GaneaFib : Type _
GaneaFib = fiber GaneaMap (pt B)

GaneaFib→join-unc' : (x : fib-cofib) → join (fib-gen (GaneaMap x)) (GaneaMap x ≡ GaneaMap x)
GaneaFib→join-unc' (inl x) = inr refl
GaneaFib→join-unc' (inr x) = inl (x , refl)
GaneaFib→join-unc' (push (a , p) i) = push (a , (λ t → p (~ i ∧ t))) refl (~ i)

GaneaFib→join-unc : (x : fib-cofib) (b : fst B) → GaneaMap x ≡ b → join (fib-gen b) (b ≡ b)
GaneaFib→join-unc x = J> GaneaFib→join-unc' x

other-gen : (b : fst B) → join (fiber (fst f) b) (b ≡ b) → GaneaFib
other-gen b (inl x) = (inr (fst x)) , {!snd x!}
other-gen b (inr x) = {!!}
other-gen b (push a b₁ i) = {!!}

other-fill : (a : fib⋆ .fst) (p : Ω B .fst) → (i j k : I) → fst B
other-fill a b i j k =
hfill (λ k → λ {(i = i0) → snd a j
; (i = i1) → b (j ∨ ~ k)
; (j = i0) → compPath-filler (snd a) (sym b) k i
; (j = i1) → snd B})
(inS (snd a (j ∨ i)))
k

other : join (fib⋆ .fst) (Ω B .fst) → GaneaFib
other (inl x) = inr (fst x) , snd x
other (inr x) = (inl tt) , x
proj₁ (other (push a b i)) = (push (fst a , snd a ∙ sym b)) (~ i) --
snd (other (push a b i)) j = other-fill a b i j i1

c1 : (i j k : I) → (a : fst A) (q : fst f a ≡ pt B) (p : q (~ i) ≡ pt B)
→ fst B
c1 i j k a q p =
hfill (λ k
→ λ {(i = i0) → p j -- p (j ∧ k)
; (i = i1) → compPath-filler' (sym q) p k j -- p j
; (j = i0) → q (k ∨ ~ i) -- pt B
; (j = i1) → pt B}) -- p k})
(inS (p j)) -- (inS (q (~ i ∨ ~ j)))
k

c2 : (i k : I) → (a : fst A) (q : fst f a ≡ pt B) (p : q (~ i) ≡ pt B)
→ join (fib⋆ .fst) (Ω B .fst)
c2 i k a q p =
hfill (λ k → λ {(i = i0) → inr p
; (i = i1) → push (a , p) (sym q ∙ p) (~ k)})
(inS (inr λ j → c1 i j i1 a q p)) k

GaneaFib→join : GaneaFib → join (fib⋆ .fst) (Ω B .fst)
GaneaFib→join (inl x , p) = inr p
GaneaFib→join (inr x , p) = inl (x , p)
GaneaFib→join (push (a , q) i , p) = c2 i i1 a q p

cancel : (x : GaneaFib) → other (GaneaFib→join x) ≡ x
cancel (inl x , y) = refl
cancel (inr x , y) = refl
cancel (push (a , q) i , p) j =
hcomp (λ k → λ {(i = i0) → inl tt , p
; (i = i1) → mg p k j
; (j = i0) → other (c2 i k a q p)
; (j = i1) → push (a , q) i , p})
((push (a , q) (i ∧ j))
, λ k → hcomp (λ r → λ {(i = i0) → p k
; (i = i1) → compPath-filler' (sym q) p (r ∧ (~ j)) k
; (j = i0) → c1 i k r a q p
; (j = i1) → p k
; (k = i0) → q ((r ∧ ~ j) ∨ ~ i)
; (k = i1) → snd B})
(p k))
where
fill1 : (i j k : I) (p : fst f a ≡ pt B)
→ fst B
fill1 i j k p =
hfill (λ k → λ {(i = i0) → compPath-filler p (sym (sym q ∙ p)) k j
; (i = i1) → q (j ∨ ~ k)
; (j = i0) → q (~ k ∧ i)
; (j = i1) → ((λ i₂ → q (~ i₂)) ∙ p) (~ k ∧ ~ i)})
(inS (compPath-filler (sym q) p j (~ i))) k

lazy : ∀ {ℓ} {A : Type ℓ} {x : A} (y : A) (q : x ≡ y) (z : A) (p : x ≡ z)
→ PathP (λ k → Square (λ j → q (j ∨ ~ k)) refl
(compPath-filler' (λ i₂ → q (~ i₂)) p (~ k)) (sym q ∙ p))
(λ i _ → (sym q ∙ p) i) λ i j → compPath-filler' (sym q) p j i
lazy {x = x} = J> (J> h x refl (refl ∙ refl) (compPath-filler' (sym refl) refl))
where
h : ∀ {ℓ} {A : Type ℓ} {x : A} (y : A) (p : x ≡ y) (q : x ≡ y) (r : p ≡ q)
→ PathP (λ k → Square refl refl (r (~ k)) q) (λ i _ → q i) λ i j → r j i
h = J> (J> refl)

lazy2 : ∀ {ℓ} {A : Type ℓ} {x : A} (y : A) (q : x ≡ y) (z : A) (p : x ≡ z)
→ PathP (λ r → Square (λ i → compPath-filler' (sym q) p i r) (λ i → (sym q ∙ p) (r ∨ ~ i)) (λ j → p (r ∨ j)) refl)
(λ j i → compPath-filler (sym q) p j (~ i))
refl
lazy2 {x = x} = J> (J> λ i j k → {!lazy x refl _ refl (~ i) k (~ j)!})

help : (p : fst f a ≡ pt B)
→ cong other (push (a , p) (sym q ∙ p))
≡ λ i → (push (a , q) (~ i)) , (compPath-filler' (sym q) p i)
proj₁ (help p i j) = push (a , λ j → fill1 i j i1 p) (~ j)
snd (help p i j) r =
hcomp (λ k → λ {(i = i0) → other-fill (a , p) (sym q ∙ p) j r k
; (i = i1) → lazy _ q _ p k r j -- compPath-filler'-filler (sym q) p j r k
; (j = i0) → compPath-filler' (sym q) p (~ k ∧ i) r
; (j = i1) → (sym q ∙ p) (r ∨ ~ (k ∨ i))
; (r = i0) → fill1 i j k p
; (r = i1) → snd B})
(lazy2 _ q _ p r j i)
{-
r = i0 ⊢
r = i1 ⊢ snd B
j = i0 ⊢ p r
j = i1 ⊢ hcomp (doubleComp-faces (λ _ → snd B) p r) (q (~ r))
i = i0 ⊢ hcomp
(λ { k (j = i0) → p r
; k (j = i1)
→ hcomp (doubleComp-faces (λ _ → snd B) p (r ∨ ~ k))
(q (~ (r ∨ ~ k)))
; k (r = i0)
→ compPath-filler p
(λ i₂ →
hcomp (doubleComp-faces (λ _ → snd B) p (~ i₂)) (q (~ (~ i₂))))
k j
; k (r = i1) → snd B
})
(p (r ∨ j))
i = i1 ⊢ hcomp
(λ { k (r = i0) → q (~ (~ j))
; k (r = i1) → p k
; k (j = i0) → p (r ∧ k)
})
(q (~ r ∧ j))
-}
{-
hcomp (λ k → λ {(i = i0) → {!c2 j i1 a p (sym q ∙ p)!}
; (i = i1) → {!!}
; (j = i0) → {!!}
; (j = i1) → {!!}})
{!!} -}
-- other (push (a , p) (sym q ∙ p) j)
open import Cubical.Foundations.Path

mg : (p : fst f a ≡ pt B)
→ PathP (λ k → other (push (a , p) (sym q ∙ p) (~ k)) ≡ (inr a , p))
(λ i → push (a , q) i , compPath-filler' (sym q) p (~ i))
refl
mg p = flipSquare (cong sym (help p)
◁ λ j i → push (a , q) (j ∨ i)
, compPath-filler' (sym q) p (~ (j ∨ i)))

cool : PathP (λ j → other {!c2 i i1 a q !} ≡ {!!}) {!!} {!!}
cool = {!j = i0 ⊢ inr a , p
j = i1 ⊢ inl tt , sym q ∙ p
i = i0 ⊢ other (push (a , p) (sym q ∙ p) j)
i = i1 ⊢ push (a , q) (~ j) , compPath-filler' (sym q) p j!}


{-
Goal: join GaneaFib (Ω B .proj₁)
———— Boundary (wanted) —————————————————————————————————————
i = i0 ⊢ inr b
i = i1 ⊢ inl (inr a , b)
-}
{- help a p i b
where
help : (a : fst A) (p : fst f a ≡ pt B)
→ PathP (λ i → (b : (p (~ i) ≡ pt B)) → join GaneaFib (Ω B .fst))
inr
λ b → inl (inr a , b)
help a p = {!!} -}

-- (sym (push {!!} {!!}) ∙∙ {!!} ∙∙ {!!}) i -- push ((inr (fst a)) , {!a!}) {!!} (~ i)

lem : join GaneaFib (Ω B .fst) → GaneaFib
lem (inl x) = x
lem (inr x) = inl tt , x
lem (push (inl x , p) b i) = (push ((pt A) , (snd f ∙ p)) ∙ sym (push ((pt A) , (snd f ∙ b)))) i , {!!}
lem (push (inr x , p) b i) = {!i = i0 ⊢ inr b
i = i1 ⊢ inl (inr a , b)!}
lem (push (push a i₁ , p) b i) = {!!}
14 changes: 0 additions & 14 deletions Cubical/HITs/SmashProduct/Ganea.agda
View file

This file was deleted.

Loading

0 comments on commit ea75092

Please sign in to comment.