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 _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
27   Definition hom_covariant     {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr _)⁻¹ >>> ((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.
32      unfold hom_covariant.
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.
37      apply qq.
38      Qed.
40   (*
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.
43      etransitivity.
44      unfold hom_covariant.
45      unfold hom_contravariant.
46      Defined.
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 ).
54     Defined.
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;
59               destruct f';
60               destruct H;
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 ]).
64     abstract (
65       destruct a; unfold YonedaBiFunctor_fmor;
66       unfold hom_covariant;
67       unfold hom_contravariant;
68       etransitivity; simpl;
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 ]
72         ]
73       | apply left_identity ]
74       ).
75     abstract (destruct a; destruct b; destruct c;
76               destruct f;
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;
83               simpl;
84               apply comp_respects;
85               reflexivity).
86     Defined.
88   Definition HomFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
89   *)
91   Definition HomFunctor   (X:ec) : Functor ec     V (ehom X).
92     refine {| fmor := @hom_covariant X |}.
93     intros.
94       unfold hom_covariant.
95       apply comp_respects; try reflexivity.
96       apply comp_respects; try reflexivity.
97       apply fmor_respects; auto.
98     intros.
99       unfold hom_covariant.
100       apply (epic _ (iso_epic ((pmon_cancelr) (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).
107     intros.
108       symmetry.
109       apply hom_covariant_distributes.
110       Defined.
112   (*
113   Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f).
114     simpl.
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.
127     simpl in 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.
133     setoid_rewrite 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.
140     simpl in qqq.
141     setoid_rewrite <- qqq.
142     setoid_rewrite <- associativity.
143     set (coincide pmon_triangle) as qqqq.
144     setoid_rewrite qqqq.
145     setoid_rewrite iso_comp1.
146     setoid_rewrite left_identity.
147     set (@eqv_equivalence) as qmt.
148     apply qmt.
149     Qed.
150     *)
152 End RepresentableStructure.
153 Opaque HomFunctor.