-
Notifications
You must be signed in to change notification settings - Fork 2
/
whiskering.v
139 lines (96 loc) · 3.6 KB
/
whiskering.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
(** **********************************************************
Benedikt Ahrens, Chris Kapulkin, Mike Shulman
january 2013
************************************************************)
(** **********************************************************
Contents :
- Precomposition with a functor for
- functors and
- natural transformations (whiskering)
- Functoriality of precomposition
- Precomposition with an essentially surjective
functor yields a faithful functor
************************************************************)
Require Import Foundations.Generalities.uu0.
Require Import Foundations.hlevel1.hProp.
Require Import Foundations.hlevel2.hSet.
Require Import RezkCompletion.pathnotations.
Import RezkCompletion.pathnotations.PathNotations.
Require Import RezkCompletion.auxiliary_lemmas_HoTT.
Require Import RezkCompletion.precategories.
Require Import RezkCompletion.functors_transformations.
Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )).
Local Notation "a --> b" := (precategory_morphisms a b)(at level 50).
(*Local Notation "'hom' C" := (precategory_morphisms (C := C)) (at level 2).*)
Local Notation "f ;; g" := (compose f g)(at level 50).
Notation "[ C , D ]" := (functor_precategory C D).
Local Notation "# F" := (functor_on_morphisms F)(at level 3).
Definition functor_compose (A B C : precategory) (F : ob [A, B])
(G : ob [B , C]) : ob [A , C] :=
functor_composite _ _ _ F G.
Local Notation "G 'O' F" := (functor_compose _ _ _ F G) (at level 25).
Local Notation "G 'o' F" := (functor_compose _ _ _ F G : functor _ _ ) (at level 25).
(** * Whiskering: Composition of a natural transformation with a functor *)
(** Prewhiskering *)
Lemma is_nat_trans_pre_whisker (A B C : precategory) (F : functor A B)
(G H : functor B C) (gamma : nat_trans G H) :
is_nat_trans (G o F) (H o F)
(fun a : ob A => gamma (F a)).
Proof.
unfold is_nat_trans.
intros; simpl;
rewrite nat_trans_ax.
apply idpath.
Qed.
Definition pre_whisker (A B C : precategory) (F : ob [A, B])
(G H : ob [B, C]) (gamma : G --> H) : G O F --> H O F.
Proof.
exists (fun a => pr1 gamma (pr1 F a)).
apply is_nat_trans_pre_whisker.
Defined.
(** Postwhiskering *)
Lemma is_precat_fun_fun_post_whisker (B C D : precategory)
(G H : functor B C) (gamma : nat_trans G H)
(K : functor C D):
is_nat_trans (functor_composite _ _ _ G K)
(functor_composite _ _ _ H K)
(fun b : B => #K (gamma b)).
Proof.
unfold is_nat_trans.
simpl in *.
intros;
repeat rewrite <- functor_comp.
rewrite (nat_trans_ax gamma).
apply idpath.
Qed.
Definition post_whisker (B C D : precategory)
(G H : ob [B, C]) (gamma : G --> H)
(K : ob [C, D]) : K O G --> K O H.
Proof.
exists (fun a : ob B => #(pr1 K) (pr1 gamma a)).
apply is_precat_fun_fun_post_whisker.
Defined.
(** Precomposition with a functor is functorial *)
(** Postcomposition is, too, but that's not of our concern for now. *)
Definition pre_composition_functor_data (A B C : precategory)
(H : ob [A, B]) : functor_data [B,C] [A,C].
Proof.
exists (fun G => G O H).
exact (fun a b gamma => pre_whisker _ _ _ H _ _ gamma).
Defined.
Lemma pre_composition_is_functor (A B C : precategory) (H : [A, B]) :
is_functor (pre_composition_functor_data A B C H).
Proof.
split; simpl.
intro G.
apply nat_trans_eq.
intro a. apply idpath.
intros; apply nat_trans_eq.
intro; apply idpath.
Qed.
Definition pre_composition_functor (A B C : precategory) (H : [A , B]) :
functor [B, C] [A, C].
Proof.
exists (pre_composition_functor_data A B C H).
apply pre_composition_is_functor.
Defined.