Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

I-indexed coproducts in pType #1907

Merged
merged 2 commits into from
Apr 13, 2024
Merged

I-indexed coproducts in pType #1907

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e0a74eb
I-indexed coproducts in pType
Alizter Apr 8, 2024
cff20ad
Apply suggestions from code review
Alizter Apr 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 39 additions & 6 deletions theories/Homotopy/Wedge.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,14 +194,14 @@ Proof.
exact pt.
Defined.

Definition fwedge_in' (I : Type) (X : I -> pType)
: forall i, X i $-> FamilyWedge I X
:= fun i => Build_pMap _ _ (fun x => pushl (i; x)) (pglue i).

(** We have an inclusion map [pushl : sig X -> FamilyWedge X]. When [I] is pointed, so is [sig X], and then this inclusion map is pointed. *)
Definition fwedge_in (I : pType) (X : I -> pType)
: psigma (pointed_fam X) $-> FamilyWedge I X.
Proof.
snrapply Build_pMap.
- exact pushl.
- exact (pglue pt).
Defined.
: psigma (pointed_fam X) $-> FamilyWedge I X
:= Build_pMap _ _ pushl (pglue pt).

(** Recursion principle for the wedge of an indexed family of pointed types. *)
Definition fwedge_rec (I : Type) (X : I -> pType) (Z : pType)
Expand Down Expand Up @@ -230,6 +230,39 @@ Proof.
- exact pconst.
Defined.

Global Instance hasallcoproducts_ptype : HasAllCoproducts pType.
Proof.
intros I X.
snrapply Build_Coproduct.
- exact (FamilyWedge I X).
- exact (fwedge_in' I X).
- exact (fwedge_rec I X).
- intros Z f i.
snrapply Build_pHomotopy.
1: reflexivity.
simpl.
apply moveL_pV.
apply equiv_1p_q1.
symmetry.
exact (Pushout_rec_beta_pglue Z _ (unit_name pt) (fun i => point_eq (f i)) _).
- intros Z f g h.
snrapply Build_pHomotopy.
+ snrapply Pushout_ind.
* intros [i x].
nrapply h.
* intros [].
exact (point_eq _ @ (point_eq _)^).
* intros i; cbn.
nrapply transport_paths_FlFr'.
lhs nrapply concat_p_pp.
apply moveR_pV.
rhs nrapply concat_pp_p.
apply moveL_pM.
symmetry.
exact (dpoint_eq (h i)).
+ reflexivity.
Defined.

(** ** The pinch map on the suspension *)

(** Given a suspension, there is a natural map from the suspension to the wedge of the suspension with itself. This is known as the pinch map.
Expand Down
Loading