forked from HoTT/Coq-HoTT
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathWedge.v
152 lines (136 loc) · 4.17 KB
/
Wedge.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
Require Import Basics Types.
Require Import Pointed.Core.
Require Import Colimits.Pushout.
Require Import WildCat.
(* Here we define the Wedge sum of two pointed types *)
Local Open Scope pointed_scope.
Definition Wedge (X Y : pType) : pType
:= [Pushout (fun _ : Unit => point X) (fun _ => point Y), pushl (point X)].
Notation "X \/ Y" := (Wedge X Y) : pointed_scope.
Definition wedge_inl {X Y} : X $-> X \/ Y.
Proof.
snrapply Build_pMap.
- exact (fun x => pushl x).
- reflexivity.
Defined.
Definition wedge_inr {X Y} : Y $-> X \/ Y.
Proof.
snrapply Build_pMap.
- exact (fun x => pushr x).
- symmetry.
by rapply pglue.
Defined.
Definition wglue {X Y : pType}
: pushl (point X) = (pushr (point Y) : X \/ Y) := pglue tt.
Definition wedge_rec {X Y Z : pType} (f : X $-> Z) (g : Y $-> Z)
: X \/ Y $-> Z.
Proof.
snrapply Build_pMap.
- snrapply Pushout_rec.
+ exact f.
+ exact g.
+ by pelim f g.
- exact (point_eq f).
Defined.
Definition wedge_incl {X Y : pType} : X \/ Y -> X * Y :=
Pushout_rec _ (fun x => (x, point Y)) (fun y => (point X, y))
(fun _ : Unit => idpath).
(** 1-universal property of wedge. *)
(** TODO: remove rewrites. For some reason pelim is not able to immediately abstract the goal so some shuffling around is necessery. *)
Lemma wedge_up X Y Z (f g : X \/ Y $-> Z)
: f $o wedge_inl $== g $o wedge_inl
-> f $o wedge_inr $== g $o wedge_inr
-> f $== g.
Proof.
intros p q.
snrapply Build_pHomotopy.
- snrapply (Pushout_ind _ p q).
intros [].
simpl.
refine (transport_paths_FlFr _ _ @ _).
refine (concat_pp_p _ _ _ @ _).
apply moveR_Vp.
refine (whiskerR (dpoint_eq p) _ @ _).
refine (_ @ whiskerL _ (dpoint_eq q)^).
clear p q.
simpl.
apply moveL_Mp.
rewrite ? ap_V.
rewrite ? inv_pp.
hott_simpl.
- simpl; pelim p q.
hott_simpl.
Defined.
Global Instance hasbinarycoproducts : HasBinaryCoproducts pType.
Proof.
intros X Y.
snrapply Build_BinaryCoproduct.
- exact (X \/ Y).
- exact wedge_inl.
- exact wedge_inr.
- intros Z f g.
by apply wedge_rec.
- intros Z f g.
snrapply Build_pHomotopy.
1: reflexivity.
by simpl; pelim f.
- intros Z f g.
snrapply Build_pHomotopy.
1: reflexivity.
simpl.
apply moveL_pV.
apply moveL_pM.
refine (_ @ (ap_V _ (pglue tt))^).
apply moveR_Mp.
apply moveL_pV.
apply moveR_Vp.
refine (Pushout_rec_beta_pglue _ f g _ _ @ _).
simpl.
by pelim f g.
- intros Z f g p q.
by apply wedge_up.
Defined.
(** Wedge of an indexed family of pointed types *)
(** Note that the index type is not necesserily pointed. An empty wedge is the unit type which is the zero object in the category of pointed types. *)
Definition FamilyWedge (I : Type) (X : I -> pType) : pType.
Proof.
snrapply Build_pType.
- srefine (Pushout (A := I) (B := sig X) (C := pUnit) _ _).
+ exact (fun i => (i; pt)).
+ exact (fun _ => pt).
- apply pushr.
exact pt.
Defined.
(** 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.
(** Recursion principle for the wedge of an indexed family of pointed types. *)
Definition fwedge_rec (I : Type) (X : I -> pType) (Z : pType)
(f : forall i, X i $-> Z)
: FamilyWedge I X $-> Z.
Proof.
snrapply Build_pMap.
- snrapply Pushout_rec.
+ apply (sig_rec _ _ _ f).
+ exact pconst.
+ intros i.
exact (point_eq (f i)).
- exact idpath.
Defined.
(** Wedge inclusions into the product can be defined if the indexing type has decidable paths. This is because we need to choose which factor a given wedge should land. This makes it somewhat awkward to work with, however in practice we typically only care about decidable index sets. *)
Definition fwedge_incl `{Funext} (I : Type) `(DecidablePaths I) (X : I -> pType)
: FamilyWedge I X $-> pproduct X.
Proof.
snrapply fwedge_rec.
intro i.
snrapply pproduct_corec.
intro a.
destruct (dec_paths i a).
- destruct p; exact pmap_idmap.
- exact pconst.
Defined.