fix typo
[coq-categories.git] / src / RepresentableStructure_ch7_2.v
1 (*******************************************************************************)
2 (* Chapter 7.2: Representable Structure                                        *)
3 (*******************************************************************************)
4
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import Categories_ch1_3.
8 Require Import Functors_ch1_4.
9 Require Import Isomorphisms_ch1_5.
10 Require Import ProductCategories_ch1_6_1.
11 Require Import OppositeCategories_ch1_6_2.
12 Require Import Enrichment_ch2_8.
13 Require Import Subcategories_ch7_1.
14 Require Import NaturalTransformations_ch7_4.
15 Require Import NaturalIsomorphisms_ch7_5.
16 Require Import MonoidalCategories_ch7_8.
17 Require Import Coherence_ch7_8.
18
19 (* FIXME: an object is a Generator if its covariant representable functor is faithful *)
20
21 Section RepresentableStructure.
22   Context `(ec:ECategory(mn:=mn)(V:=V)).
23
24   Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell mn _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
25   Definition hom_covariant     {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr mn _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
26
27   Lemma hom_covariant_distributes     {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
28      : hom_covariant (f >>> g) ~~ (hom_covariant (a:=x) f) >>> (hom_covariant g).
29      set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
30      unfold hom_covariant.
31      repeat setoid_rewrite associativity.
32      apply comp_respects; try reflexivity.
33      set (@ecomp_is_functorial) as qq.
34      repeat setoid_rewrite associativity in qq.
35      apply qq.
36      Qed.
37
38   Lemma hom_contravariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
39      : hom_contravariant (f >>> g) ~~ (hom_contravariant g) >>> (hom_contravariant (a:=x) f).
40      set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
41      unfold hom_contravariant.
42      repeat setoid_rewrite associativity.
43      etransitivity; [ idtac | symmetry; apply associativity ].
44      apply comp_respects; try reflexivity.
45      set (@ecomp_is_functorial _ _ _ _ _ _ _ _ _ _ _ _ _ x f g) as qq.
46      setoid_rewrite juggle2 in qq.
47      admit.
48      Qed.
49
50   Lemma hom_swap {a b c d:ec}(f:a~~{ec}~~>b)(g:c~~{ec}~~>d)
51      : hom_covariant f >>> hom_contravariant g ~~ hom_contravariant g >>> hom_covariant f.
52      etransitivity.
53      unfold hom_covariant.
54      unfold hom_contravariant.
55      Admitted.
56
57   Definition YonedaBiFunctor_fmor (a b:ec⁽ºᑭ⁾ ×× ec)(f:a~~{ec⁽ºᑭ⁾ ×× ec}~~>b)
58         : ((fst_obj _ _ a)~~>(snd_obj _ _ a))~~{V}~~>((fst_obj _ _ b)~~>(snd_obj _ _ b)).
59     destruct a as [a1 a2].
60     destruct b as [b1 b2].
61     case f as [f1 f2]; intros.
62     exact ( hom_contravariant (a:=a2) f1 >>> hom_covariant (a:=b1) f2 ).
63     Defined.
64
65   Definition YonedaBiFunctor : Functor (ec⁽ºᑭ⁾ ×× ec) V (fun a => (fst_obj _ _ a)~~>(snd_obj _ _ a)).
66     refine {| fmor := fun a b f => YonedaBiFunctor_fmor a b f |}.
67     abstract (intros; destruct a; destruct b; destruct f;
68               destruct f';
69               destruct H;
70               repeat (apply comp_respects; try reflexivity); simpl;
71               [ apply (@fmor_respects _ _ _ _ _ _ (fun x => (bin_obj x _))); auto
72               | apply (fmor_respects ((o1 ~~> o0) ⋊-)); auto ]).
73     abstract (
74       destruct a; unfold YonedaBiFunctor_fmor;
75       unfold hom_covariant;
76       unfold hom_contravariant;
77       etransitivity; simpl;
78       [ apply comp_respects; setoid_rewrite associativity; simpl;
79         [ etransitivity; [ apply comp_respects; [ reflexivity | apply eleft_identity ] | apply iso_comp2 ]
80         | etransitivity; [ apply comp_respects; [ reflexivity | apply eright_identity ] | apply iso_comp2 ]
81         ]
82       | apply left_identity ]
83       ).
84     abstract (destruct a; destruct b; destruct c;
85               destruct f;
86               destruct g; unfold YonedaBiFunctor_fmor;
87               setoid_rewrite juggle3;
88               setoid_rewrite hom_swap;
89               setoid_rewrite <- juggle3;
90               setoid_rewrite <- hom_contravariant_distributes;
91               setoid_rewrite <- hom_covariant_distributes;
92               simpl;
93               apply comp_respects;
94               reflexivity).
95     Defined.
96
97   Definition RepresentableFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
98   Definition RepresentableFunctor   (X:ec) : Functor ec     V (fun a => X~~>a) :=
99     func_llecnac(C:=ec⁽ºᑭ⁾)(D:=ec) X >>>> YonedaBiFunctor.
100   
101   Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (RepresentableFunctor a \ f).
102     simpl.
103     setoid_rewrite <- associativity.
104     unfold hom_contravariant.
105     repeat setoid_rewrite <- associativity.
106     setoid_rewrite juggle1.
107     setoid_rewrite eleft_identity.
108     repeat setoid_rewrite <- associativity.
109     setoid_rewrite juggle1.
110     setoid_rewrite iso_comp1.
111     setoid_rewrite right_identity.
112     unfold hom_covariant.
113     repeat setoid_rewrite <- associativity.
114     set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (eid a)) as qq.
115     simpl in qq.
116     apply iso_shift_right' in qq.
117     apply symmetry in qq.
118     setoid_rewrite <- associativity in qq.
119     apply iso_shift_left' in qq.
120     apply symmetry in qq.
121     setoid_rewrite qq.
122     setoid_rewrite associativity.
123     setoid_rewrite juggle3.
124     setoid_rewrite (centralmor_first(CentralMorphism:=eid_central(ECategory:=ec) a)).
125     repeat setoid_rewrite associativity.
126     setoid_rewrite eleft_identity.
127     set (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn) f) as qqq.
128     simpl in qqq.
129     setoid_rewrite <- qqq.
130     setoid_rewrite <- associativity.
131     set (coincide pmon_triangle) as qqqq.
132     setoid_rewrite qqqq.
133     setoid_rewrite iso_comp1.
134     setoid_rewrite left_identity.
135     set (@eqv_equivalence) as qmt.
136     apply qmt.
137     Qed.
138
139
140 End RepresentableStructure.
141 Opaque RepresentableFunctor.
142
143 Structure MonoidalEnrichment {e:Enrichment} :=
144 { me_enr         :=e
145 ; me_fobj        : prod_obj e e -> e
146 ; me_f           : Functor (e ×× e) e me_fobj
147 ; me_i           : e
148 ; me_mon         : MonoidalCat e me_fobj me_f me_i
149 ; me_mf          : MonoidalFunctor me_mon (enr_v_mon e) (RepresentableFunctor e me_i)
150 }.
151 Implicit Arguments MonoidalEnrichment [ ].
152 Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
153 Coercion me_enr : MonoidalEnrichment >-> Enrichment.
154
155 (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
156 Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
157 { ffme_enr             := me
158 ; ffme_mf_full         : FullFunctor         (RepresentableFunctor e (me_i me))
159 ; ffme_mf_faithful     : FaithfulFunctor     (RepresentableFunctor e (me_i me))
160 ; ffme_mf_conservative : ConservativeFunctor (RepresentableFunctor e (me_i me))
161 }.
162 Implicit Arguments MonicMonoidalEnrichment [ ].
163 Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
164 Transparent RepresentableFunctor.
165
166 Lemma CartesianEnrMonoidal (e:Enrichment) `(C:CartesianCat(Ob:= _)(Hom:= _)(C:=Underlying (enr_c e))) : MonoidalEnrichment e.
167   admit.
168   Defined.
169
170 Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
171 { smme_se       : SurjectiveEnrichment e
172 ; smme_monoidal : MonoidalEnrichment e
173 ; smme_me       : MonicMonoidalEnrichment _ smme_monoidal
174 }.
175 Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
176 Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
177
178 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
179 Structure SMME :=
180 { smme_e   : Enrichment
181 ; smme_mon : MonoidalEnrichment smme_e
182 ; smme_mee : MonicMonoidalEnrichment _ smme_mon
183 }.
184 Coercion smme_e   : SMME >-> Enrichment.
185 Coercion smme_mon : SMME >-> MonoidalEnrichment.
186 Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.