You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
(** The quotient of a graph is one of the simplest HITs that can be found in HoTT. It consists of a base type and a relation on it, and for every witness of a relation between two points of the type, a path.
9
+
10
+
We use graph quotients to build up all our other non-recursive HITs. Their simplicity means that we can easily prove results about them and generalise them to other HITs. *)
11
+
5
12
LocalUnset Elimination Schemes.
6
13
7
14
ModuleExport GraphQuotient.
@@ -38,7 +45,6 @@ End GraphQuotient.
38
45
39
46
Arguments gq {A R} a.
40
47
41
-
42
48
Definition GraphQuotient_rec {A R P} (c : A -> P) (g : forall a b, R a b -> c a = c b)
43
49
: GraphQuotient R -> P.
44
50
Proof.
@@ -58,3 +64,161 @@ Proof.
58
64
refine ((apD_const _ _)^ @ _).
59
65
rapply GraphQuotient_ind_beta_gqglue.
60
66
Defined.
67
+
68
+
(** ** The flattening lemma *)
69
+
70
+
(** Univalence tells us that type families over a colimit correspond to cartesian families over the indexing diagram. The flattening lemma gives an explicit description of the family over a colimit that corresponds to a given cartesian family, again using univalence. Together, these are known as descent, a fundamental result in higher topos theory which has many implications. *)
71
+
72
+
Section Flattening.
73
+
74
+
Context `{Univalence} {A : Type} {R : A -> A -> Type}.
75
+
(** We consider a type family over [A] which is "equifibrant" or "cartesian": the fibers are equivalent when the base points are related by [R]. *)
76
+
Context (F : A -> Type) (e : forall x y, R x y -> F x <~> F y).
77
+
78
+
(** By univalence, the equivalences give equalities, which means that [F] induces a map on the quotient. *)
79
+
Definition DGraphQuotient : GraphQuotient R -> Type
80
+
:= GraphQuotient_rec F (fun x y s => path_universe (e x y s)).
81
+
82
+
(** The transport of [DGraphQuotient] along [gqglue] equals the equivalence [e] applied to the original point. This lemma is required a few times in the following proofs. *)
83
+
Definition transport_DGraphQuotient {x y} (s : R x y) (a : F x)
84
+
: transport DGraphQuotient (gqglue s) a = e x y s a.
85
+
Proof.
86
+
lhs nrapply transport_idmap_ap.
87
+
lhs nrapply (transport2 idmap).
88
+
1: apply GraphQuotient_rec_beta_gqglue.
89
+
rapply transport_path_universe.
90
+
Defined.
91
+
92
+
(** The family [DGraphQuotient] we have defined over [GraphQuotient R] has a total space which we will describe as a [GraphQuotient] of [sig F] by an appropriate relation. *)
93
+
94
+
(** We mimic the constructors of [GraphQuotient] for the total space. Here is the point constructor. *)
95
+
Definition flatten_gq {x} : F x -> sig DGraphQuotient.
96
+
Proof.
97
+
intros p.
98
+
exact (gq x; p).
99
+
Defined.
100
+
101
+
(** And here is the path constructor. *)
102
+
Definition flatten_gqglue {x y} (s : R x y) (a : F x)
103
+
: flatten_gq a = flatten_gq (e x y s a).
104
+
Proof.
105
+
snrapply path_sigma'.
106
+
- by apply gqglue.
107
+
- apply transport_DGraphQuotient.
108
+
Defined.
109
+
110
+
(** This lemma is the same as [transport_DGraphQuotient] but adapted instead for [DPath]. The use of [DPath] will be apparent there. *)
111
+
Lemma equiv_dp_dgraphquotient (x y : A) (s : R x y) (a : F x) (b : F y)
112
+
: DPath DGraphQuotient (gqglue s) a b <~> (e x y s a = b).
113
+
Proof.
114
+
refine (_ oE dp_path_transport^-1).
115
+
refine (equiv_concat_l _^ _).
116
+
apply transport_DGraphQuotient.
117
+
Defined.
118
+
119
+
(** We can also prove an induction principle for [sig DGraphQuotient]. We won't show that it satisfies the relevant computation rules as these will not be needed. Instead we will prove the non-dependent eliminator directly so that we can better reason about it. In order to get through the path algebra here, we have opted to use dependent paths. This makes the reasoning slightly easier, but it should not matter too much. *)
120
+
Definition flatten_ind {Q : sig DGraphQuotient -> Type}
121
+
(Qgq : forall a (x : F a), Q (flatten_gq x))
122
+
(Qgqglue : forall a b (s : R a b) (x : F a),
123
+
flatten_gqglue s x # Qgq _ x = Qgq _ (e _ _ _ x))
124
+
: forall x, Q x.
125
+
Proof.
126
+
apply sig_ind.
127
+
snrapply GraphQuotient_ind.
128
+
1: exact Qgq.
129
+
intros a b s.
130
+
apply equiv_dp_path_transport.
131
+
apply dp_forall.
132
+
intros x y.
133
+
srapply (equiv_ind (equiv_dp_dgraphquotient a b s x y)^-1).
134
+
intros q.
135
+
destruct q.
136
+
apply equiv_dp_path_transport.
137
+
refine (transport2 _ _ _ @ Qgqglue a b s x).
138
+
refine (ap (path_sigma_uncurried DGraphQuotient _ _) _).
139
+
snrapply path_sigma.
140
+
1: reflexivity.
141
+
apply moveR_equiv_V.
142
+
simpl; f_ap.
143
+
lhs rapply concat_p1.
144
+
rapply inv_V.
145
+
Defined.
146
+
147
+
(** Rather than use [flatten_ind] to define [flatten_rec] we reprove this simple case. This means we can later reason about it and derive the computation rules easily. The full computation rule for [flatten_ind] takes some work to derive and is not actually needed. *)
148
+
Definition flatten_rec {Q : Type} (Qgq : forall a, F a -> Q)
149
+
(Qgqglue : forall a b (s : R a b) (x : F a), Qgq a x = Qgq b (e _ _ s x))
150
+
: sig DGraphQuotient -> Q.
151
+
Proof.
152
+
apply sig_rec.
153
+
snrapply GraphQuotient_ind.
154
+
1: exact Qgq.
155
+
intros a b s.
156
+
nrapply dpath_arrow.
157
+
intros y.
158
+
lhs nrapply transport_const.
159
+
lhs nrapply (Qgqglue a b s).
160
+
f_ap; symmetry.
161
+
apply transport_DGraphQuotient.
162
+
Defined.
163
+
164
+
(** The non-dependent eliminator computes as expected on our "path constructor". *)
165
+
Definition flatten_rec_beta_gqglue {Q : Type} (Qgq : forall a, F a -> Q)
166
+
(Qgqglue : forall a b (r : R a b) (x : F a), Qgq a x = Qgq b (e _ _ r x))
167
+
(a b : A) (s : R a b) (x : F a)
168
+
: ap (flatten_rec Qgq Qgqglue) (flatten_gqglue s x) = Qgqglue a b s x.
(** Now that we've shown that [sig DGraphQuotient] acts like a [GraphQuotient] of [sig F] by an appropriate relation, we can use this to prove the flattening lemma. The maps back and forth are very easy so this could almost be a formal consequence of the induction principle. *)
187
+
Lemma equiv_gq_flatten
188
+
: sig DGraphQuotient
189
+
<~> GraphQuotient (fun a b => {r : R a.1 b.1 & e _ _ r a.2 = b.2}).
Copy file name to clipboardExpand all lines: theories/Types/Sigma.v
+2-4Lines changed: 2 additions & 4 deletions
Original file line number
Diff line number
Diff line change
@@ -311,15 +311,13 @@ Proof.
311
311
Defined.
312
312
313
313
314
-
(** Applying a function constructed with [sig_ind] to a [path_sigma] can be computed. Technically this computation should probably go by way of a 2-variable [ap], and should be done in the dependently typed case. *)
315
-
314
+
(** Applying a function constructed with [sig_rec] to a [path_sigma] can be computed. Technically this computation should probably go by way of a 2-variable [ap], and should be done in the dependently typed case. *)
0 commit comments