-
Notifications
You must be signed in to change notification settings - Fork 2
/
category_hset.v
235 lines (162 loc) · 5.18 KB
/
category_hset.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
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
(** **********************************************************
Benedikt Ahrens, Chris Kapulkin, Mike Shulman
january 2013
************************************************************)
(** **********************************************************
Contents :
Precategory HSET of hSets
HSET is a category
************************************************************)
Require Import Foundations.Generalities.uu0.
Require Import Foundations.hlevel1.hProp.
Require Import Foundations.hlevel2.hSet.
Require Import Foundations.Proof_of_Extensionality.funextfun.
Require Import RezkCompletion.auxiliary_lemmas_HoTT.
Require Import RezkCompletion.precategories.
Require Import RezkCompletion.HLevel_n_is_of_hlevel_Sn.
Require Import RezkCompletion.pathnotations.
Import RezkCompletion.pathnotations.PathNotations.
Local Notation "a --> b" := (precategory_morphisms a b)(at level 50).
(** * Precategory of hSets *)
Lemma isaset_set_fun_space (A B : hSet) : isaset (A -> B).
Proof.
change isaset with (isofhlevel 2).
apply impred.
apply (fun _ => (pr2 B)).
Qed.
Definition hset_fun_space (A B : hSet) : hSet :=
hSetpair _ (isaset_set_fun_space A B).
Definition hset_precategory_ob_mor : precategory_ob_mor :=
tpair (fun ob : UU => ob -> ob -> hSet) hSet
(fun A B : hSet => hset_fun_space A B).
Definition hset_precategory_data : precategory_data :=
precategory_data_pair hset_precategory_ob_mor (fun (A:hSet) (x : A) => x)
(fun (A B C : hSet) (f : A -> B) (g : B -> C) (x : A) => g (f x)).
Lemma is_precategory_hset_precategory_data :
is_precategory hset_precategory_data.
Proof.
repeat split; simpl.
Qed.
Definition hset_precategory : precategory :=
tpair _ _ is_precategory_hset_precategory_data.
Notation HSET := hset_precategory.
(*
Canonical Structure hset_precategory. :-)
*)
(** * The precategory of hSets is a category. *)
(** ** Equivalence between isomorphisms and weak equivalences
of two hsets.
*)
(** Given an iso, we construct a weak equivalence.
This is basically unpacking and packing again.
*)
Lemma hset_iso_is_equiv (A B : ob HSET)
(f : iso A B) : isweq (pr1 f).
Proof.
destruct f as [f fax]; simpl in *.
apply (gradth _ (pr1 fax)).
destruct fax as [g [eta eps]]; simpl in *.
unfold compose, identity in *;
simpl in *.
intro x.
apply (toforallpaths _ _ _ eta).
destruct fax as [g [eta eps]]; simpl in *.
unfold compose, identity in *;
simpl in *.
intro x.
apply (toforallpaths _ _ _ eps).
Defined.
Lemma hset_iso_equiv (A B : ob HSET) : iso A B -> weq (pr1 A) (pr1 B).
Proof.
intro f.
exists (pr1 f).
apply hset_iso_is_equiv.
Defined.
(** Given a weak equivalence, we construct an iso.
Again mostly unwrapping and packing.
*)
Lemma hset_equiv_is_iso (A B : hSet)
(f : weq (pr1 A) (pr1 B)) :
is_isomorphism (C:=HSET) (pr1 f).
Proof.
exists (invmap f).
split; simpl.
apply funextfunax; intro x; simpl in *.
unfold compose, identity; simpl.
apply homotinvweqweq.
apply funextfunax; intro x; simpl in *.
unfold compose, identity; simpl.
apply homotweqinvweq.
Defined.
Lemma hset_equiv_iso (A B : ob HSET) : weq (pr1 A) (pr1 B) -> iso A B.
Proof.
intro f.
simpl in *.
exists (pr1 f).
apply hset_equiv_is_iso.
Defined.
(** Both maps defined above are weak equivalences. *)
Lemma hset_iso_equiv_is_equiv (A B : ob HSET) : isweq (hset_iso_equiv A B).
Proof.
apply (gradth _ (hset_equiv_iso A B)).
intro; apply eq_iso; reflexivity.
intro; apply total2_paths_hProp.
intro; apply isapropisweq.
reflexivity.
Qed.
Definition hset_iso_equiv_weq (A B : ob HSET) : weq (iso A B) (weq (pr1 A) (pr1 B)).
Proof.
exists (hset_iso_equiv A B).
apply hset_iso_equiv_is_equiv.
Defined.
Lemma hset_equiv_iso_is_equiv (A B : ob HSET) : isweq (hset_equiv_iso A B).
Proof.
apply (gradth _ (hset_iso_equiv A B)).
intro f.
apply total2_paths_hProp.
apply isapropisweq.
reflexivity.
intro; apply eq_iso.
reflexivity.
Qed.
Definition hset_equiv_iso_weq (A B : ob HSET) :
weq (weq (pr1 A) (pr1 B))(iso A B).
Proof.
exists (hset_equiv_iso A B).
apply hset_equiv_iso_is_equiv.
Defined.
(** ** HSET is a category. *)
Definition univalenceweq (X X' : UU) : weq (X == X') (weq X X') :=
tpair _ _ (univalenceaxiom X X').
Definition hset_id_iso_weq (A B : ob HSET) :
weq (A == B) (iso A B) :=
weqcomp (UA_for_HLevels 2 A B) (hset_equiv_iso_weq A B).
(** The map [precat_paths_to_iso]
for which we need to show [isweq] is actually
equal to the carrier of the weak equivalence we
constructed above.
We use this fact to show that that [precat_paths_to_iso]
is an equivalence.
*)
Lemma hset_id_iso_weq_is (A B : ob HSET):
@idtoiso _ A B == pr1 (hset_id_iso_weq A B).
Proof.
apply funextfunax.
intro p; elim p.
apply eq_iso; simpl.
apply funextfun;
intro x;
destruct A.
apply idpath.
Defined.
Lemma is_weq_precat_paths_to_iso_hset (A B : ob HSET):
isweq (@idtoiso _ A B).
Proof.
rewrite hset_id_iso_weq_is.
apply (pr2 (hset_id_iso_weq A B)).
Defined.
Lemma is_category_HSET : is_category HSET.
Proof.
unfold is_category.
apply is_weq_precat_paths_to_iso_hset.
Defined.