{-# OPTIONS --without-K --rewriting #-}
open import lib.Basics
open import lib.cubical.Square
open import lib.types.Bool
open import lib.types.Cofiber
open import lib.types.Lift
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.PushoutFmap
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Suspension
open import lib.types.Wedge
module lib.types.BigWedge where
module _ {i j} {A : Type i} where
bigwedge-f : (X : A → Ptd j) → A → Σ A (de⊙ ∘ X)
bigwedge-f X a = a , pt (X a)
bigwedge-span : (A → Ptd j) → Span
bigwedge-span X = cofiber-span (bigwedge-f X)
BigWedge : (A → Ptd j) → Type (lmax i j)
BigWedge X = Cofiber (bigwedge-f X)
bwbase : {X : A → Ptd j} → BigWedge X
bwbase = cfbase
bwin : {X : A → Ptd j} → (a : A) → de⊙ (X a) → BigWedge X
bwin = curry cfcod
⊙BigWedge : (A → Ptd j) → Ptd (lmax i j)
⊙BigWedge X = ⊙[ BigWedge X , bwbase ]
bwglue : {X : A → Ptd j} → (a : A) → bwbase {X} == bwin a (pt (X a))
bwglue = cfglue
⊙bwin : {X : A → Ptd j} → (a : A) → X a ⊙→ ⊙BigWedge X
⊙bwin a = (bwin a , ! (bwglue a))
module BigWedgeElim {X : A → Ptd j} {k} {P : BigWedge X → Type k}
(base* : P bwbase) (in* : (a : A) (x : de⊙ (X a)) → P (bwin a x))
(glue* : (a : A) → base* == in* a (pt (X a)) [ P ↓ bwglue a ])
= CofiberElim {f = bigwedge-f X} {P = P} base* (uncurry in*) glue*
BigWedge-elim = BigWedgeElim.f
module BigWedgeRec {X : A → Ptd j} {k} {C : Type k}
(base* : C) (in* : (a : A) → de⊙ (X a) → C)
(glue* : (a : A) → base* == in* a (pt (X a)))
= CofiberRec {f = bigwedge-f X} {C = C} base* (uncurry in*) glue*
module _ {i j₀ j₁} {A : Type i} {X₀ : A → Ptd j₀} {X₁ : A → Ptd j₁}
(Xeq : ∀ a → X₀ a ⊙≃ X₁ a) where
bigwedge-span-emap-r : SpanEquiv (cofiber-span (bigwedge-f X₀)) (cofiber-span (bigwedge-f X₁))
bigwedge-span-emap-r = span-map (idf _) (Σ-fmap-r λ a → fst (⊙–> (Xeq a))) (idf _)
(comm-sqr λ _ → idp) (comm-sqr λ a → pair= idp (⊙–>-pt (Xeq a))) ,
idf-is-equiv _ , Σ-isemap-r (λ a → snd (Xeq a)) , idf-is-equiv _
BigWedge-emap-r : BigWedge X₀ ≃ BigWedge X₁
BigWedge-emap-r = Pushout-emap bigwedge-span-emap-r
⊙BigWedge-emap-r : ⊙BigWedge X₀ ⊙≃ ⊙BigWedge X₁
⊙BigWedge-emap-r = ≃-to-⊙≃ BigWedge-emap-r idp
module _ {i₀ i₁ j} {A₀ : Type i₀} {A₁ : Type i₁}
(X : A₁ → Ptd j) (Aeq : A₀ ≃ A₁) where
bigwedge-span-emap-l : SpanEquiv (cofiber-span (bigwedge-f (X ∘ –> Aeq))) (cofiber-span (bigwedge-f X))
bigwedge-span-emap-l = span-map (idf _) (Σ-fmap-l (de⊙ ∘ X) (–> Aeq)) (–> Aeq)
(comm-sqr λ _ → idp) (comm-sqr λ _ → idp) ,
idf-is-equiv _ , Σ-isemap-l (de⊙ ∘ X) (snd Aeq) , snd Aeq
BigWedge-emap-l : BigWedge (X ∘ –> Aeq) ≃ BigWedge X
BigWedge-emap-l = Pushout-emap bigwedge-span-emap-l
⊙BigWedge-emap-l : ⊙BigWedge (X ∘ –> Aeq) ⊙≃ ⊙BigWedge X
⊙BigWedge-emap-l = ≃-to-⊙≃ BigWedge-emap-l idp
module _ {i} {A : Type i} (X : A → Ptd i) where
extract-glue-from-BigWedge-is-const :
∀ bw → extract-glue {s = bigwedge-span X} bw == north
extract-glue-from-BigWedge-is-const = BigWedge-elim
idp
(λ x y → ! (merid x))
(↓-='-from-square ∘ λ x →
ExtractGlue.glue-β x ∙v⊡
tr-square (merid x)
⊡v∙ ! (ap-cst north (cfglue x)))
module _ {i} (Pick : Bool → Ptd i) where
BigWedge-Bool-equiv-Wedge : BigWedge Pick ≃ Wedge (Pick true) (Pick false)
BigWedge-Bool-equiv-Wedge = equiv f g f-g g-f
where
module F = BigWedgeRec {X = Pick}
{C = Wedge (Pick true) (Pick false)}
(winl (pt (Pick true)))
(λ {true → winl; false → winr})
(λ {true → idp; false → wglue})
module G = WedgeRec {X = Pick true} {Y = Pick false}
{C = BigWedge Pick}
(bwin true)
(bwin false)
(! (bwglue true) ∙ bwglue false)
f = F.f
g = G.f
abstract
f-g : ∀ w → f (g w) == w
f-g = Wedge-elim
(λ _ → idp)
(λ _ → idp)
(↓-∘=idf-in' f g $
ap f (ap g wglue)
=⟨ ap (ap f) G.glue-β ⟩
ap f (! (bwglue true) ∙ bwglue false)
=⟨ ap-∙ f (! (bwglue true)) (bwglue false) ⟩
ap f (! (bwglue true)) ∙ ap f (bwglue false)
=⟨ ap-! f (bwglue true)
|in-ctx (λ w → w ∙ ap f (bwglue false)) ⟩
! (ap f (bwglue true)) ∙ ap f (bwglue false)
=⟨ F.glue-β true
|in-ctx (λ w → ! w ∙ ap f (bwglue false)) ⟩
ap f (bwglue false)
=⟨ F.glue-β false ⟩
wglue =∎)
g-f : ∀ bw → g (f bw) == bw
g-f = BigWedge-elim
(! (bwglue true))
(λ {true → λ _ → idp; false → λ _ → idp})
(λ {true → ↓-∘=idf-from-square g f $
ap (ap g) (F.glue-β true) ∙v⊡
bl-square (bwglue true);
false → ↓-∘=idf-from-square g f $
(ap (ap g) (F.glue-β false) ∙ G.glue-β) ∙v⊡
lt-square (! (bwglue true)) ⊡h vid-square})