-
Notifications
You must be signed in to change notification settings - Fork 1
/
CommutativeSquares.v
113 lines (102 loc) · 3.73 KB
/
CommutativeSquares.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
(*******************************************************************************
Title: CommutativeSquares.v
Authors: Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine
Date: 1 March 2013
Some basic results on commutative squares, considered as maps of
arrows.
*******************************************************************************)
Require Import HoTT.
Require Import Auxiliary.
Section Comm_Squares.
(* Commutative squares compose. *)
Lemma comm_square_comp
{A B} {f:A->B} {A' B'} {f':A'->B'} {A'' B''} {f'':A''->B''}
{h' : A' -> A''} {g' : B' -> B''} (comm' : f'' o h' == g' o f')
{h : A -> A'} {g : B -> B'} (comm : f' o h == g o f)
: f'' o (h' o h) == (g' o g) o f.
Proof.
intros x. path_via (g' (f' (h x))).
apply ap, comm.
Defined.
(* We show that given any commutative square from [f] to [f'] whose verticals
[wA, wB] are equivalences, the equiv_inv square from [f'] to [f] with verticals
[wA ^-1, wB ^-1] also commutes. *)
Lemma comm_square_inverse
{A B : Type} {f : A -> B}
{A' B' : Type} {f' : A' -> B'}
{wA : A <~> A'} {wB : B <~> B'}
(wf : f' o wA == wB o f)
: f o (wA ^-1) == (wB ^-1) o f'.
Proof.
intros a'.
path_via (wB ^-1 (wB (f (wA ^-1 a')))).
apply inverse, eissect.
apply ap, (concat (wf _)^).
apply ap, eisretr.
Defined.
(* Up to naturality, the result of [comm_square_inverse] really is a
retraction (aka left inverse); *)
Lemma comm_square_inverse_is_sect
{A B : Type} {f : A -> B}
{A' B' : Type} {f' : A' -> B'}
(wA : A <~> A') (wB : B <~> B')
(wf : f' o wA == wB o f)
: (fun a:A => (comm_square_comp (comm_square_inverse wf) wf a)
@ eissect wB (f a))
== fun a:A => (ap f (eissect wA a)).
Proof.
intros a; simpl. unfold comm_square_inverse, comm_square_comp; simpl.
repeat apply (concat (concat_pp_p)). apply moveR_Vp.
path_via' (ap (wB ^-1 o wB) (ap f (eissect wA a)) @ eissect wB (f a)).
Focus 2. apply (concat (concat_Ap (eissect wB) _)). apply ap, ap_idmap.
apply (concat (concat_p_pp)), whiskerR.
apply (concat (ap_pp (wB ^-1) _ _)^), (concatR (ap_compose wB _ _)^).
apply ap, (concat concat_pp_p), moveR_Vp.
path_via (ap (f' o wA) (eissect wA a) @ wf a).
apply whiskerR. apply (concatR (ap_compose wA f' _)^).
apply ap, eisadj.
apply (concat (concat_Ap wf _)).
apply whiskerL, (ap_compose f wB).
Defined.
(* and similarly, [comm_square_inverse] is a section (aka right equiv_inv). *)
(* TODO (low) : simplify proof!? *)
Lemma comm_square_inverse_is_retr
{A B : Type} {f : A -> B}
{A' B' : Type} {f' : A' -> B'}
(wA : A <~> A') (wB : B <~> B')
(wf : f' o wA == wB o f)
: (fun a:A' => (comm_square_comp wf (comm_square_inverse wf) a)
@ eisretr wB (f' a))
== fun a:A' => (ap f' (eisretr wA a)).
Proof.
intros a; simpl. unfold comm_square_inverse, comm_square_comp; simpl.
rewrite !ap_pp. rewrite <- !concat_pp_p.
rewrite concat_pp_p.
set (p := (ap wB (ap (wB ^-1) (ap f' (eisretr wA a)))
@ eisretr wB (f' a))).
path_via ((eisretr wB _)^ @ p).
apply whiskerR.
apply moveR_pM.
path_via ((eisretr wB (f' (wA (wA ^-1 a))))^ @
ap (wB o wB ^-1) (wf ((wA ^-1) a))).
rewrite ap_V. rewrite <- eisadj.
path_via' (ap idmap (wf ((wA ^-1) a))
@ (eisretr wB (wB (f ((wA ^-1) a))))^).
apply whiskerR. apply inverse. apply ap_idmap.
apply (concat_Ap
(fun b' => (eisretr wB b')^) (wf ((wA ^-1) a)) ).
apply ap. rewrite ap_compose. rewrite !ap_V.
apply inverse. apply inv_V.
apply moveR_Vp. subst p. rewrite <- ap_compose.
path_via (eisretr wB (f' (wA ((wA ^-1) a)))
@ ap idmap (ap f' (eisretr wA a))).
apply (concat_Ap
(eisretr wB) (ap f' (eisretr wA a)) ).
apply ap. apply ap_idmap.
Defined.
End Comm_Squares.
(*
Local Variables:
coq-prog-name: "hoqtop"
End:
*)