-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathloop_spaces.v
65 lines (49 loc) · 1.54 KB
/
loop_spaces.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
Require Import HoTT.Homotopy.
Require Import pointed_spaces.
Set Implicit Arguments.
Unset Strict Implicit.
Import pointed_spaces.pt_map_notation.
Definition loop_space_type (X : pt_type) : Type := point X = point X.
Definition loop_space (X : pt_type) : pt_type :=
{| carrier := loop_space_type X ;
point := idpath |}.
Section loop_space_functorial.
Variables X Y : pt_type.
Variable f : X .-> Y.
Definition loop_space_map_carrier (* (X Y : pt_type) (f : pt_map X Y)*) :
loop_space_type X -> loop_space_type Y :=
fun p =>
!pt_map_point f @ map f p @ pt_map_point f.
Definition loop_space_map_refl :
loop_space_map_carrier idpath = idpath.
Proof.
unfold loop_space_map_carrier.
rewrite idpath_map.
apply opposite_left_inverse.
Defined.
Definition loop_space_map_concat (p q : loop_space_type X) :
loop_space_map_carrier (p @ q) =
loop_space_map_carrier p @ loop_space_map_carrier q.
Proof.
transitivity (!pt_map_point f @ map f p @ map f q @ pt_map_point f).
unfold loop_space_map_carrier.
apply whisker_left.
rewrite concat_map.
rewrite concat_associativity.
reflexivity.
unfold loop_space_map_carrier.
repeat rewrite concat_associativity.
apply whisker_left.
apply whisker_left.
repeat rewrite <- concat_associativity.
apply whisker_right.
(* rewrite concat_associativity. *)
rewrite opposite_right_inverse.
reflexivity.
Defined.
Definition loop_space_map : loop_space X .-> loop_space Y.
exists loop_space_map_carrier.
simpl.
exact loop_space_map_refl.
Defined.
End loop_space_functorial.