1 (*******************************************************************************)
2 (* Chapter 7.2: Representable Structure *)
3 (*******************************************************************************)
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 EpicMonic_ch2_1.
11 Require Import ProductCategories_ch1_6_1.
12 Require Import OppositeCategories_ch1_6_2.
13 Require Import Enrichment_ch2_8.
14 Require Import Subcategories_ch7_1.
15 Require Import NaturalTransformations_ch7_4.
16 Require Import NaturalIsomorphisms_ch7_5.
17 Require Import MonoidalCategories_ch7_8.
18 Require Import Coherence_ch7_8.
19 Require Import BinoidalCategories.
20 Require Import PreMonoidalCategories.
21 Require Import MonoidalCategories_ch7_8.
23 Section RepresentableStructure.
24 Context `(ec:ECategory(mn:=mn)(V:=V)).
26 Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell mn _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
27 Definition hom_covariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr mn _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
29 Lemma hom_covariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
30 : hom_covariant (f >>> g) ~~ (hom_covariant (a:=x) f) >>> (hom_covariant g).
31 set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
33 repeat setoid_rewrite associativity.
34 apply comp_respects; try reflexivity.
35 set (@ecomp_is_functorial) as qq.
36 repeat setoid_rewrite associativity in qq.
41 Lemma hom_swap {a b c d:ec}(f:a~~{ec}~~>b)(g:c~~{ec}~~>d)
42 : hom_covariant f >>> hom_contravariant g ~~ hom_contravariant g >>> hom_covariant f.
45 unfold hom_contravariant.
48 Definition YonedaBiFunctor_fmor (a b:ec⁽ºᑭ⁾ ×× ec)(f:a~~{ec⁽ºᑭ⁾ ×× ec}~~>b)
49 : ((fst_obj _ _ a)~~>(snd_obj _ _ a))~~{V}~~>((fst_obj _ _ b)~~>(snd_obj _ _ b)).
50 destruct a as [a1 a2].
51 destruct b as [b1 b2].
52 case f as [f1 f2]; intros.
53 exact ( hom_contravariant (a:=a2) f1 >>> hom_covariant (a:=b1) f2 ).
56 Definition YonedaBiFunctor : Functor (ec⁽ºᑭ⁾ ×× ec) V (fun a => (fst_obj _ _ a)~~>(snd_obj _ _ a)).
57 refine {| fmor := fun a b f => YonedaBiFunctor_fmor a b f |}.
58 abstract (intros; destruct a; destruct b; destruct f;
61 repeat (apply comp_respects; try reflexivity); simpl;
62 [ apply (@fmor_respects _ _ _ _ _ _ (fun x => (bin_obj x _))); auto
63 | apply (fmor_respects ((o1 ~~> o0) ⋊-)); auto ]).
65 destruct a; unfold YonedaBiFunctor_fmor;
67 unfold hom_contravariant;
69 [ apply comp_respects; setoid_rewrite associativity; simpl;
70 [ etransitivity; [ apply comp_respects; [ reflexivity | apply eleft_identity ] | apply iso_comp2 ]
71 | etransitivity; [ apply comp_respects; [ reflexivity | apply eright_identity ] | apply iso_comp2 ]
73 | apply left_identity ]
75 abstract (destruct a; destruct b; destruct c;
77 destruct g; unfold YonedaBiFunctor_fmor;
78 setoid_rewrite juggle3;
79 setoid_rewrite hom_swap;
80 setoid_rewrite <- juggle3;
81 setoid_rewrite <- hom_contravariant_distributes;
82 setoid_rewrite <- hom_covariant_distributes;
88 Definition HomFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
91 Definition HomFunctor (X:ec) : Functor ec V (ehom X).
92 refine {| fmor := @hom_covariant X |}.
95 apply comp_respects; try reflexivity.
96 apply comp_respects; try reflexivity.
97 apply fmor_respects; auto.
100 apply (epic _ (iso_epic ((pmon_cancelr mn) (X ~~> a)))).
101 setoid_rewrite <- associativity.
102 setoid_rewrite <- associativity.
103 setoid_rewrite iso_comp1.
104 setoid_rewrite left_identity.
105 setoid_rewrite right_identity.
106 apply (@eright_identity).
109 apply hom_covariant_distributes.
113 Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f).
115 setoid_rewrite <- associativity.
116 unfold hom_contravariant.
117 repeat setoid_rewrite <- associativity.
118 setoid_rewrite juggle1.
119 setoid_rewrite eleft_identity.
120 repeat setoid_rewrite <- associativity.
121 setoid_rewrite juggle1.
122 setoid_rewrite iso_comp1.
123 setoid_rewrite right_identity.
124 unfold hom_covariant.
125 repeat setoid_rewrite <- associativity.
126 set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (eid a)) as qq.
128 apply iso_shift_right' in qq.
129 apply symmetry in qq.
130 setoid_rewrite <- associativity in qq.
131 apply iso_shift_left' in qq.
132 apply symmetry in qq.
134 setoid_rewrite associativity.
135 setoid_rewrite juggle3.
136 setoid_rewrite (centralmor_first(CentralMorphism:=eid_central(ECategory:=ec) a)).
137 repeat setoid_rewrite associativity.
138 setoid_rewrite eleft_identity.
139 set (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn) f) as qqq.
141 setoid_rewrite <- qqq.
142 setoid_rewrite <- associativity.
143 set (coincide pmon_triangle) as qqqq.
145 setoid_rewrite iso_comp1.
146 setoid_rewrite left_identity.
147 set (@eqv_equivalence) as qmt.
152 End RepresentableStructure.
155 Structure MonoidalEnrichment {e:Enrichment} :=
157 ; me_fobj : prod_obj e e -> e
158 ; me_f : Functor (e ×× e) e me_fobj
160 ; me_mon : MonoidalCat e me_fobj me_f me_i
161 ; me_mf : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i)
163 Implicit Arguments MonoidalEnrichment [ ].
164 Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
165 Coercion me_enr : MonoidalEnrichment >-> Enrichment.
167 (* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
168 Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
170 ; ffme_mf_full : FullFunctor (HomFunctor e (me_i me))
171 ; ffme_mf_faithful : FaithfulFunctor (HomFunctor e (me_i me))
172 ; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me))
174 Implicit Arguments MonicMonoidalEnrichment [ ].
175 Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
176 Transparent HomFunctor.
178 Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
179 { smme_se : SurjectiveEnrichment e
180 ; smme_monoidal : MonoidalEnrichment e
181 ; smme_me : MonicMonoidalEnrichment _ smme_monoidal
183 Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
184 Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
186 (* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
188 { smme_e : Enrichment
189 ; smme_see : SurjectiveEnrichment smme_e
190 ; smme_mon : MonoidalEnrichment smme_e
191 ; smme_mee : MonicMonoidalEnrichment _ smme_mon
193 Coercion smme_e : SMME >-> Enrichment.
194 Coercion smme_see : SMME >-> SurjectiveEnrichment.
195 Coercion smme_mon : SMME >-> MonoidalEnrichment.
196 Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.