263 lines
12 KiB
Text
263 lines
12 KiB
Text
/-
|
||
Copyright (c) 2016 Jakob von Raumer. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Floris van Doorn
|
||
|
||
The Wedge Sum of a family of Pointed Types
|
||
-/
|
||
import homotopy.wedge ..move_to_lib ..choice ..pointed_pi
|
||
|
||
open eq is_equiv pushout pointed unit trunc_index sigma bool equiv trunc choice unit is_trunc sigma.ops lift function
|
||
|
||
definition fwedge' {I : Type} (F : I → Type*) : Type := pushout (λi, ⟨i, Point (F i)⟩) (λi, ⋆)
|
||
definition pt' [constructor] {I : Type} {F : I → Type*} : fwedge' F := inr ⋆
|
||
definition fwedge [constructor] {I : Type} (F : I → Type*) : Type* := pointed.MK (fwedge' F) pt'
|
||
|
||
notation `⋁` := fwedge
|
||
|
||
namespace fwedge
|
||
variables {I : Type} {F : I → Type*}
|
||
|
||
definition il {i : I} (x : F i) : ⋁F := inl ⟨i, x⟩
|
||
definition inl (i : I) (x : F i) : ⋁F := il x
|
||
definition pinl [constructor] (i : I) : F i →* ⋁F := pmap.mk (inl i) (glue i)
|
||
definition glue (i : I) : inl i pt = pt :> ⋁ F := glue i
|
||
|
||
protected definition rec {P : ⋁F → Type} (Pinl : Π(i : I) (x : F i), P (il x))
|
||
(Pinr : P pt) (Pglue : Πi, pathover P (Pinl i pt) (glue i) (Pinr)) (y : fwedge' F) : P y :=
|
||
begin induction y, induction x, apply Pinl, induction x, apply Pinr, apply Pglue end
|
||
|
||
protected definition elim {P : Type} (Pinl : Π(i : I) (x : F i), P)
|
||
(Pinr : P) (Pglue : Πi, Pinl i pt = Pinr) (y : fwedge' F) : P :=
|
||
begin induction y with x u, induction x with i x, exact Pinl i x, induction u, apply Pinr, apply Pglue end
|
||
|
||
protected definition elim_glue {P : Type} {Pinl : Π(i : I) (x : F i), P}
|
||
{Pinr : P} (Pglue : Πi, Pinl i pt = Pinr) (i : I)
|
||
: ap (fwedge.elim Pinl Pinr Pglue) (fwedge.glue i) = Pglue i :=
|
||
!pushout.elim_glue
|
||
|
||
protected definition rec_glue {P : ⋁F → Type} {Pinl : Π(i : I) (x : F i), P (il x)}
|
||
{Pinr : P pt} (Pglue : Πi, pathover P (Pinl i pt) (glue i) (Pinr)) (i : I)
|
||
: apd (fwedge.rec Pinl Pinr Pglue) (fwedge.glue i) = Pglue i :=
|
||
!pushout.rec_glue
|
||
|
||
end fwedge
|
||
|
||
attribute fwedge.rec fwedge.elim [recursor 7] [unfold 7]
|
||
attribute fwedge.il fwedge.inl [constructor]
|
||
|
||
namespace fwedge
|
||
|
||
definition fwedge_of_pwedge [unfold 3] {A B : Type*} (x : A ∨ B) : ⋁(bool.rec A B) :=
|
||
begin
|
||
induction x with a b,
|
||
{ exact inl ff a },
|
||
{ exact inl tt b },
|
||
{ exact glue ff ⬝ (glue tt)⁻¹ }
|
||
end
|
||
|
||
definition pwedge_of_fwedge [unfold 3] {A B : Type*} (x : ⋁(bool.rec A B)) : A ∨ B :=
|
||
begin
|
||
induction x with b x b,
|
||
{ induction b, exact pushout.inl x, exact pushout.inr x },
|
||
{ exact pushout.inr pt },
|
||
{ induction b, exact pushout.glue ⋆, reflexivity }
|
||
end
|
||
|
||
definition pwedge_pequiv_fwedge [constructor] (A B : Type*) : A ∨ B ≃* ⋁(bool.rec A B) :=
|
||
begin
|
||
fapply pequiv_of_equiv,
|
||
{ fapply equiv.MK,
|
||
{ exact fwedge_of_pwedge },
|
||
{ exact pwedge_of_fwedge },
|
||
{ exact abstract begin intro x, induction x with b x b,
|
||
{ induction b: reflexivity },
|
||
{ exact glue tt },
|
||
{ apply eq_pathover_id_right,
|
||
refine ap_compose fwedge_of_pwedge _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
|
||
induction b, exact !elim_glue ⬝ph whisker_bl _ hrfl, apply square_of_eq idp }
|
||
end end },
|
||
{ exact abstract begin intro x, induction x with a b,
|
||
{ reflexivity },
|
||
{ reflexivity },
|
||
{ apply eq_pathover_id_right,
|
||
refine ap_compose pwedge_of_fwedge _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝
|
||
!elim_glue ◾ (!ap_inv ⬝ !elim_glue⁻²) ⬝ph _, exact hrfl } end end}},
|
||
{ exact glue ff }
|
||
end
|
||
|
||
definition is_contr_fwedge_of_neg {I : Type} (P : I → Type*) (H : ¬ I) : is_contr (⋁P) :=
|
||
begin
|
||
apply is_contr.mk pt, intro x, induction x, contradiction, reflexivity, contradiction
|
||
end
|
||
|
||
definition is_contr_fwedge_empty [instance] : is_contr (⋁empty.elim) :=
|
||
is_contr_fwedge_of_neg _ id
|
||
|
||
definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X :=
|
||
begin
|
||
fconstructor,
|
||
{ intro x, induction x,
|
||
exact f i x,
|
||
exact pt,
|
||
exact respect_pt (f i) },
|
||
{ reflexivity }
|
||
end
|
||
|
||
definition fwedge_pmap_beta [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) (i : I) :
|
||
fwedge_pmap f ∘* pinl i ~* f i :=
|
||
begin
|
||
fconstructor,
|
||
{ reflexivity },
|
||
{ exact !idp_con ⬝ !fwedge.elim_glue⁻¹ }
|
||
end
|
||
|
||
definition fwedge_pmap_eta [constructor] {I : Type} {F : I → Type*} {X : Type*} (g : ⋁F →* X) :
|
||
fwedge_pmap (λi, g ∘* pinl i) ~* g :=
|
||
begin
|
||
fconstructor,
|
||
{ intro x, induction x,
|
||
reflexivity,
|
||
exact (respect_pt g)⁻¹,
|
||
apply eq_pathover, refine !elim_glue ⬝ph _, apply whisker_lb, exact hrfl },
|
||
{ exact con.left_inv (respect_pt g) }
|
||
end
|
||
|
||
definition fwedge_pmap_pinl [constructor] {I : Type} {F : I → Type*} : fwedge_pmap (λi, pinl i) ~* pid (⋁ F) :=
|
||
begin
|
||
fconstructor,
|
||
{ intro x, induction x,
|
||
reflexivity, reflexivity,
|
||
apply eq_pathover, apply hdeg_square, refine !elim_glue ⬝ !ap_id⁻¹ },
|
||
{ reflexivity }
|
||
end
|
||
|
||
definition fwedge_pmap_equiv [constructor] {I : Type} (F : I → Type*) (X : Type*) :
|
||
⋁F →* X ≃ Πi, F i →* X :=
|
||
begin
|
||
fapply equiv.MK,
|
||
{ intro g i, exact g ∘* pinl i },
|
||
{ exact fwedge_pmap },
|
||
{ intro f, apply eq_of_homotopy, intro i, apply eq_of_phomotopy, apply fwedge_pmap_beta f i },
|
||
{ intro g, apply eq_of_phomotopy, exact fwedge_pmap_eta g }
|
||
end
|
||
|
||
definition fwedge_pmap_nat₂ {I : Type}(F : I → Type*){X Y : Type*}
|
||
(f : X →* Y) (h : Πi, F i →* X) (w : fwedge F) :
|
||
(f ∘* (fwedge_pmap h)) w = fwedge_pmap (λi, f ∘* (h i)) w :=
|
||
begin
|
||
induction w, reflexivity,
|
||
refine !respect_pt,
|
||
apply eq_pathover,
|
||
refine ap_compose f (fwedge_pmap h) _ ⬝ph _,
|
||
refine ap (ap f) !elim_glue ⬝ph _,
|
||
refine _ ⬝hp !elim_glue⁻¹, esimp,
|
||
apply whisker_br,
|
||
apply !hrefl
|
||
end
|
||
|
||
definition fwedge_pmap_phomotopy {I : Type} {F : I → Type*} {X : Type*} {f g : Π i, F i →* X}
|
||
(h : Π i, f i ~* g i) : fwedge_pmap f ~* fwedge_pmap g :=
|
||
begin
|
||
fconstructor,
|
||
{ fapply fwedge.rec,
|
||
{ exact h },
|
||
{ reflexivity },
|
||
{ intro i, apply eq_pathover,
|
||
refine _ ⬝ph _ ⬝hp _,
|
||
{ exact (respect_pt (g i)) },
|
||
{ exact (respect_pt (f i)) },
|
||
{ exact !elim_glue },
|
||
{ apply square_of_eq,
|
||
exact ((phomotopy.sigma_char (f i) (g i)) (h i)).2
|
||
},
|
||
{ refine !elim_glue⁻¹ }
|
||
}
|
||
},
|
||
{ reflexivity }
|
||
end
|
||
|
||
definition trunc_fwedge_pmap_equiv.{u} {n : ℕ₋₂} {I : Type.{u}} (H : has_choice n I)
|
||
(F : I → pType.{u}) (X : pType.{u}) : trunc n (⋁F →* X) ≃ Πi, trunc n (F i →* X) :=
|
||
trunc_equiv_trunc n (fwedge_pmap_equiv F X) ⬝e choice_equiv (λi, F i →* X)
|
||
|
||
|
||
definition fwedge_functor [constructor] {I : Type} {F F' : I → Type*} (f : Π i, F i →* F' i)
|
||
: ⋁ F →* ⋁ F' := fwedge_pmap (λ i, pinl i ∘* f i)
|
||
|
||
definition fwedge_functor_pid {I : Type} {F : I → Type*}
|
||
: @fwedge_functor I F F (λ i, !pid) ~* !pid :=
|
||
calc fwedge_pmap (λ i, pinl i ∘* !pid) ~* fwedge_pmap pinl : by exact fwedge_pmap_phomotopy (λ i, pcompose_pid (pinl i))
|
||
... ~* fwedge_pmap (λ i, !pid ∘* pinl i) : by exact fwedge_pmap_phomotopy (λ i, phomotopy.symm (pid_pcompose (pinl i)))
|
||
... ~* !pid : by exact fwedge_pmap_eta !pid
|
||
|
||
definition fwedge_functor_pcompose {I : Type} {F F' F'' : I → Type*} (g : Π i, F' i →* F'' i)
|
||
(f : Π i, F i →* F' i) : fwedge_functor (λ i, g i ∘* f i) ~* fwedge_functor g ∘* fwedge_functor f :=
|
||
calc fwedge_functor (λ i, g i ∘* f i)
|
||
~* fwedge_pmap (λ i, (pinl i ∘* g i) ∘* f i)
|
||
: by exact fwedge_pmap_phomotopy (λ i, phomotopy.symm (passoc (pinl i) (g i) (f i)))
|
||
... ~* fwedge_pmap (λ i, (fwedge_functor g ∘* pinl i) ∘* f i)
|
||
: by exact fwedge_pmap_phomotopy (λ i, pwhisker_right (f i) (phomotopy.symm (fwedge_pmap_beta (λ i, pinl i ∘* g i) i)))
|
||
... ~* fwedge_pmap (λ i, fwedge_functor g ∘* (pinl i ∘* f i))
|
||
: by exact fwedge_pmap_phomotopy (λ i, passoc (fwedge_functor g) (pinl i) (f i))
|
||
... ~* fwedge_pmap (λ i, fwedge_functor g ∘* (fwedge_functor f ∘* pinl i))
|
||
: by exact fwedge_pmap_phomotopy (λ i, pwhisker_left (fwedge_functor g) (phomotopy.symm (fwedge_pmap_beta (λ i, pinl i ∘* f i) i)))
|
||
... ~* fwedge_pmap (λ i, (fwedge_functor g ∘* fwedge_functor f) ∘* pinl i)
|
||
: by exact fwedge_pmap_phomotopy (λ i, (phomotopy.symm (passoc (fwedge_functor g) (fwedge_functor f) (pinl i))))
|
||
... ~* fwedge_functor g ∘* fwedge_functor f
|
||
: by exact fwedge_pmap_eta (fwedge_functor g ∘* fwedge_functor f)
|
||
|
||
definition fwedge_functor_phomotopy {I : Type} {F F' : I → Type*} {f g : Π i, F i →* F' i}
|
||
(h : Π i, f i ~* g i) : fwedge_functor f ~* fwedge_functor g :=
|
||
fwedge_pmap_phomotopy (λ i, pwhisker_left (pinl i) (h i))
|
||
|
||
definition fwedge_pequiv [constructor] {I : Type} {F F' : I → Type*} (f : Π i, F i ≃* F' i) : ⋁ F ≃* ⋁ F' :=
|
||
let pto := fwedge_functor (λ i, f i) in
|
||
let pfrom := fwedge_functor (λ i, (f i)⁻¹ᵉ*) in
|
||
begin
|
||
fapply pequiv_of_pmap, exact pto,
|
||
fapply adjointify, exact pfrom,
|
||
{ intro y, refine (fwedge_functor_pcompose (λ i, f i) (λ i, (f i)⁻¹ᵉ*) y)⁻¹ ⬝ _,
|
||
refine fwedge_functor_phomotopy (λ i, pright_inv (f i)) y ⬝ _,
|
||
exact fwedge_functor_pid y
|
||
},
|
||
{ intro y, refine (fwedge_functor_pcompose (λ i, (f i)⁻¹ᵉ*) (λ i, f i) y)⁻¹ ⬝ _,
|
||
refine fwedge_functor_phomotopy (λ i, pleft_inv (f i)) y ⬝ _,
|
||
exact fwedge_functor_pid y
|
||
}
|
||
end
|
||
|
||
definition plift_fwedge.{u v} {I : Type} (F : I → pType.{u}) : plift.{u v} (⋁ F) ≃* ⋁ (plift.{u v} ∘ F) :=
|
||
calc plift.{u v} (⋁ F) ≃* ⋁ F : by exact !pequiv_plift ⁻¹ᵉ*
|
||
... ≃* ⋁ (λ i, plift.{u v} (F i)) : by exact fwedge_pequiv (λ i, !pequiv_plift)
|
||
|
||
definition fwedge_down_left.{u v} {I : Type} (F : I → pType) : ⋁ (F ∘ down.{u v}) ≃* ⋁ F :=
|
||
proof
|
||
let pto := @fwedge_pmap (lift.{u v} I) (F ∘ down) (⋁ F) (λ i, pinl (down i)) in
|
||
let pfrom := @fwedge_pmap I F (⋁ (F ∘ down.{u v})) (λ i, pinl (up.{u v} i)) in
|
||
begin
|
||
fapply pequiv_of_pmap,
|
||
{ exact pto },
|
||
fapply adjointify,
|
||
{ exact pfrom },
|
||
{ intro x, exact calc pto (pfrom x) = fwedge_pmap (λ i, (pto ∘* pfrom) ∘* pinl i) x : by exact (fwedge_pmap_eta (pto ∘* pfrom) x)⁻¹
|
||
... = fwedge_pmap (λ i, pto ∘* (pfrom ∘* pinl i)) x : by exact fwedge_pmap_phomotopy (λ i, passoc pto pfrom (pinl i)) x
|
||
... = fwedge_pmap (λ i, pto ∘* pinl (up.{u v} i)) x : by exact fwedge_pmap_phomotopy (λ i, pwhisker_left pto (fwedge_pmap_beta (λ i, pinl (up.{u v} i)) i)) x
|
||
... = fwedge_pmap pinl x : by exact fwedge_pmap_phomotopy (λ i, fwedge_pmap_beta (λ i, (pinl (down.{u v} i))) (up.{u v} i)) x
|
||
... = x : by exact fwedge_pmap_pinl x
|
||
},
|
||
{ intro x, exact calc pfrom (pto x) = fwedge_pmap (λ i, (pfrom ∘* pto) ∘* pinl i) x : by exact (fwedge_pmap_eta (pfrom ∘* pto) x)⁻¹
|
||
... = fwedge_pmap (λ i, pfrom ∘* (pto ∘* pinl i)) x : by exact fwedge_pmap_phomotopy (λ i, passoc pfrom pto (pinl i)) x
|
||
... = fwedge_pmap (λ i, pfrom ∘* pinl (down.{u v} i)) x : by exact fwedge_pmap_phomotopy (λ i, pwhisker_left pfrom (fwedge_pmap_beta (λ i, pinl (down.{u v} i)) i)) x
|
||
... = fwedge_pmap pinl x : by exact fwedge_pmap_phomotopy (λ i,
|
||
begin induction i with i,
|
||
exact fwedge_pmap_beta (λ i, (pinl (up.{u v} i))) i
|
||
end
|
||
) x
|
||
... = x : by exact fwedge_pmap_pinl x
|
||
}
|
||
|
||
end
|
||
qed
|
||
|
||
end fwedge
|