holy shit solved leg3

This commit is contained in:
Michael Zhang 2025-01-24 05:41:25 -06:00
parent fea38f46f5
commit c7f6942d7c

View file

@ -41,33 +41,69 @@ module _ {A∙ @ (A , a₀) : Pointed } {B∙ @ (B , b₀) : Pointed } (f
P : A Type
P a = f a b₀
fw : Σ A (λ a (a a₀) × (f a b₀)) f a₀ b₀
fw (a , p , feq) = subst P p feq
fw (a , p , feq) = cong f (sym p) feq
gw : f a₀ b₀ Σ A (λ a (a a₀) × (f a b₀))
gw p = a₀ , refl , p
fg : section fw gw
fg p = substRefl {B = λ a f a b₀} p
gf : retract fw gw
-- p : f a₀ ≡ b₀
fg p = sym (lUnit p)
-- fw (gw p) ≡ p
-- fw (a₀ , refl , p) ≡ p
-- subst (λ a' → f a' ≡ b₀) refl p ≡ p
test : (feq : f a₀ b₀) subst P refl feq feq
test feq = substRefl {B = P} feq
module _ (a : A) (p : a a₀) (feq : f a b₀) where
-- bottomFace : Square (subst P p feq) (subst P refl feq) (λ i → f (p (~ i))) refl
-- bottomFace i j = subst {! !} {! !} {! !} {! !}
-- cong f (sym refl) ∙ p ≡ p
-- fg p = substRefl {B = λ a → f a ≡ b₀} p
gf : retract fw gw
gf (a , p , feq) i = p (~ i) , (λ j p (~ i j)) , λ j sq i j where
-- gw (fw (a , p , feq)) ≡ (a , p , feq)
-- gw (cong f (sym p) ∙ feq) ≡ (a , p , feq)
-- a₀ , refl , (cong f (sym p) ∙ feq) ≡ (a , p , feq)
postulate
-- TODO: FINISH THIS
topFace : Square (λ i f (p (~ i))) (λ i b₀) (subst P p feq) feq
-- topFace = {! !}
-- (cong f (λ i → p (~ i)) ∙ feq) (cong f (λ i → a) ∙ feq)
gf (a , p , feq) i = p (~ i) , (λ j p (~ i j)) , λ j topFace a p feq j i
sq : PathP (λ i f (p (~ i)) b₀) ((λ i f (p (~ i))) feq) feq
sq i j =
let u = λ k λ where
(i = i0) compPath-filler (cong f (sym p)) feq k j
(i = i1) feq (j k)
(j = i0) f (p (~ i))
(j = i1) feq k
in hcomp u (cong f (sym p) (i j))
-- -- p : f a₀ ≡ b₀
-- -- fw (gw p) ≡ p
-- -- fw (a₀ , refl , p) ≡ p
-- -- subst (λ a' → f a' ≡ b₀) refl p ≡ p
-- module _ (a : A) (p : a ≡ a₀) (feq : f a ≡ b₀) where
-- -- bottomFace : Square (subst P p feq) (subst P refl feq) (λ i → f (p (~ i))) refl
-- -- bottomFace i j = subst {! !} {! !} {! !} {! !}
-- test : PathP (λ i → a ≡ p (~ i)) p refl
-- test i j = p (~ i ∧ j)
-- test2 : f a₀ ≡ b₀
-- test2 = cong f (sym p) ∙ feq
-- test3 : f a ≡ b₀
-- test3 = refl ∙ feq
-- bottomFace : PathP (λ i → f (p (~ i)) ≡ b₀) (cong f (sym p) ∙ feq) (refl ∙ feq)
-- bottomFace = congP (λ i q → cong f (sym q) ∙ feq) test
-- topFace : PathP (λ i → f (p (~ i)) ≡ b₀) (subst P p feq) feq
-- topFace i j = hcomp u (bottomFace i j) where
-- u = λ k → λ where
-- (i = i0) → {! !}
-- (i = i1) → {! !}
-- (j = i0) → f (p (~ i))
-- (j = i1) → b₀
-- gf (a , p , feq) i = p (~ i) , (λ j → p (~ i j)) , λ j → {! !}
-- topFace a p feq i j
-- gw (fw (a , p , feq)) ≡ (a , p , feq)
-- gw (subst (λ a' → f a' ≡ b₀) p feq) ≡ (a , p , feq)
-- (a₀ , refl , p) ≡ (a , p , feq)
eq : subst P refl f₀ f₀
eq = substRefl {B = P} f₀
eq : refl f₀ f₀
eq = sym (lUnit f₀)
-- eq = substRefl {B = P} f₀
leg4 : (f a₀ b₀) , f₀ ≃∙ Ω B∙
leg4 = isoToEquiv (iso fw gw fg gf) , eq where