1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "categories.ma".
16 include "notation.ma".
18 record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type2 ≝ {
21 FP: map_objs2 ?? F F1 =_\ID F2
24 lemma REW : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀X,Y:Fo ?? F.
25 arrows2 C2 (F (F1 ??? X)) (F (F1 ??? Y)) →
26 arrows2 C2 (F2 ??? X) (F2 ??? Y).
27 intros 5; cases X; cases Y; clear X Y;
28 cases H; cases H1; intros; assumption;
31 record Fm_c (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) (X,Y:Fo ?? F) : Type2 ≝ {
32 Fm2: arrows2 C2 (F2 ??? X) (F2 ??? Y);
33 Fm1: arrows2 C1 (F1 ??? X) (F1 ??? Y);
34 FmP: REW ?? F X Y (map_arrows2 ?? F ?? Fm1) = Fm2
38 ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.
39 Fo ?? F → Fo ?? F → setoid2.
40 intros (C1 C2 F X Y); constructor 1; [apply (Fm_c C1 C2 F X Y)]
41 constructor 1; [apply (λf,g.Fm2 ????? f =_2 Fm2 ????? g);]
43 | intros 3; apply sym2; assumption;
44 | intros 5; apply (trans2 ?? ??? x1 x2);]
48 ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o.Fm ?? F o o.
49 intros; constructor 1;
50 [ apply (id2 C2 (F2 ??? o));
51 | apply (id2 C1 (F1 ??? o));
52 | cases o; cases H; simplify; apply (respects_id2 ?? F);]
56 ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o1,o2,o3.
57 binary_morphism2 (Fm ?? F o1 o2) (Fm ?? F o2 o3) (Fm ?? F o1 o3).
58 intros; constructor 1;
59 [ intros (f g); constructor 1;
60 [ apply (comp2 C2 ??? (Fm2 ????? f) (Fm2 ????? g));
61 | apply (comp2 C1 ??? (Fm1 ????? f) (Fm1 ????? g));
62 | apply hide; cases o1 in f; cases o2 in g; cases o3; clear o1 o2 o3;
63 cases H; cases H1; cases H2; intros 2; cases c; cases c1; clear c c1;
64 simplify; apply (.= (respects_comp2:?)); apply (e1‡e);]
65 | intros 6; change with
66 ((Fm2 C1 C2 F o2 o3 b∘Fm2 C1 C2 F o1 o2 a) =
67 (Fm2 C1 C2 F o2 o3 b'∘Fm2 C1 C2 F o1 o2 a'));
68 change in e1 with (Fm2 ?? F ?? b = Fm2 ?? F ?? b');
69 change in e with (Fm2 ?? F ?? a = Fm2 ?? F ?? a');
74 definition Apply : ∀C1,C2: CAT2.arrows3 CAT2 C1 C2 → CAT2.
81 | intros; apply (comp_assoc2 C2 ???? (Fm2 ????? a12) (Fm2 ????? a23) (Fm2 ????? a34));
82 | intros; apply (id_neutral_right2 C2 ?? (Fm2 ????? a));
83 | intros; apply (id_neutral_left2 C2 ?? (Fm2 ????? a));]