]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/sets/categories.ma
Use the inversion!
[helm.git] / helm / software / matita / nlibrary / sets / categories.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16 include "sets/sets.ma".
17
18 nrecord category : Type[2] ≝
19  { objs:> Type[1];
20    arrows: objs → objs → setoid;
21    id: ∀o:objs. arrows o o;
22    comp: ∀o1,o2,o3. unary_morphism (arrows o2 o3) (unary_morph_setoid (arrows o1 o2) (arrows o1 o3));
23    comp_assoc: ∀o1,o2,o3,o4. ∀a34,a23,a12.
24     comp o1 o3 o4 a34 (comp o1 o2 o3 a23 a12) = comp o1 o2 o4 (comp o2 o3 o4 a34 a23) a12;
25    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o2) a = a;
26    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a
27  }.
28
29 notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
30 interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
31 interpretation "arrows" 'arrows A B = (unary_morphism A B).
32
33 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
34 notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
35
36 interpretation "id" 'id A = (id ? A).
37
38 ndefinition SETOID : category.
39 @; 
40 ##[ napply setoid;
41 ##| napply unary_morph_setoid;
42 ##| #o; @ (λx.x); #a; #b; #H; napply H;
43 ##| napply comp_binary_morphisms; (*CSC: why not ∘?*)
44 ##| #o1; #o2; #o3; #o4; #f; #g; #h; #x; #x'; #Hx; nnormalize; napply (†(†(†Hx)))
45 ##|##6,7: #o1; #o2; #f; #x; #x'; #Hx; nnormalize; napply (†Hx) ]
46 nqed.
47
48 unification hint 0 ≔ ;
49    R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
50           (comp_assoc SETOID) (id_neutral_left SETOID)
51           (id_neutral_right SETOID))
52  (* -------------------------------------------------------------------- *) ⊢
53                               objs R ≡ setoid.
54                               
55  unification hint 0 ≔ x,y ;
56    R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
57           (comp_assoc SETOID) (id_neutral_left SETOID)
58           (id_neutral_right SETOID))
59  (* -------------------------------------------------------------------- *) ⊢
60                   arrows R x y ≡ unary_morph_setoid x y. 
61                   
62 unification hint 0 ≔ A,B ;               
63                   T ≟ (unary_morph_setoid A B)
64            (* ----------------------------------- *) ⊢              
65                   unary_morphism A B ≡ carr T. 
66                 
67                 
68 ndefinition TYPE : setoid1.
69 @ setoid; @; 
70 ##[ #T1; #T2; 
71     alias symbol "eq" = "setoid eq".
72     napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
73 ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
74 ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption; 
75 ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg'; 
76     @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
77        ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
78     @; #x;
79     ##[ napply (.= (†(Hf …))); napply Hg;
80     ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##] 
81 nqed.
82
83 unification hint 0 ≔ ;
84           R ≟ (mk_setoid1 setoid (eq1 TYPE))
85   (* -------------------------------------------- *) ⊢
86                  carr1 R ≡ setoid.
87    
88 nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
89  { fun01:1> A → B;
90    prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
91  }.
92  
93 interpretation "prop01" 'prop1 c  = (prop01 ????? c).