matita/matita/nlibrary/sets/categories2.ma

   1
   2 include "sets/sets.ma".
   3 include "sets/setoids2.ma".
   4 include "sets/categories.ma".
   5
   6 (*
   7 ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
   8 #S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
   9 ##[ #f; #g; napply (∀x,y. f x y = g x y);
  10 ##| #f; #x; #y; napply #;
  11 ##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
  12 ##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
  13 nqed.
  14
  15 ndefinition unary_morph_setoid : setoid → setoid → setoid.
  16 #S1; #S2; @ (unary_morphism S1 S2); @;
  17 ##[ #f; #g; napply (∀x. f x = g x);
  18 ##| #f; #x; napply #;
  19 ##| #f; #g; #H; #x; napply ((H x)^-1);
  20 ##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
  21 nqed.
  22
  23 nrecord category : Type[2] ≝
  24  { objs:> Type[1];
  25    arrows: objs → objs → setoid;
  26    id: ∀o:objs. arrows o o;
  27    comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
  28    comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
  29     comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
  30    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
  31    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
  32  }.
  33 *)
  34
  35 notation "hvbox(A break ⇒ B)" right associative with precedence 55 for @{ 'arrows $A $B }.
  36 interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
  37 interpretation "arrows" 'arrows A B = (unary_morphism A B).
  38
  39 (*
  40 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
  41 notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
  42
  43 interpretation "id" 'id A = (id ? A).
  44
  45 ndefinition SETOID : category.
  46 @;
  47 ##[ napply setoid;
  48 ##| napply unary_morph_setoid;
  49 ##| #o; @ (λx.x); #a; #b; #H; napply H;
  50 ##| #o1; #o2; #o3; @;
  51     ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
  52     ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x)));
  53         napply (.= (†(H1 x))); napply #; ##]
  54 ##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
  55 ##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
  56 nqed.
  57
  58 unification hint 0 ≔ ;
  59    R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
  60           (comp_assoc SETOID) (id_neutral_left SETOID)
  61           (id_neutral_right SETOID))
  62  (* -------------------------------------------------------------------- *) ⊢
  63                               objs R ≡ setoid.
  64
  65  unification hint 0 ≔ x,y ;
  66    R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
  67           (comp_assoc SETOID) (id_neutral_left SETOID)
  68           (id_neutral_right SETOID))
  69  (* -------------------------------------------------------------------- *) ⊢
  70                   arrows R x y ≡ unary_morph_setoid x y.
  71
  72 unification hint 0 ≔ A,B ;
  73                   T ≟ (unary_morph_setoid A B)
  74            (* ----------------------------------- *) ⊢
  75                   unary_morphism A B ≡ carr T.
  76
  77
  78 ndefinition TYPE : setoid1.
  79 @ setoid; @;
  80 ##[ #T1; #T2;
  81     alias symbol "eq" = "setoid eq".
  82     napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
  83 ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
  84 ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
  85 ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
  86     @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
  87        ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
  88     @; #x;
  89     ##[ napply (.= (†(Hf …))); napply Hg;
  90     ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##]
  91 nqed.
  92
  93 unification hint 0 ≔ ;
  94           R ≟ (mk_setoid1 setoid (eq1 TYPE))
  95   (* -------------------------------------------- *) ⊢
  96                  carr1 R ≡ setoid.
  97
  98 nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
  99  { fun01:1> A → B;
 100    prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
 101  }.
 102
 103 interpretation "prop01" 'prop1 c  = (prop01 ????? c).
 104 *)