2 include "sets/sets.ma".
4 nrecord category : Type[2] ≝
6 arrows: objs → objs → setoid;
7 id: ∀o:objs. arrows o o;
8 comp: ∀o1,o2,o3. binary_morphism (arrows o2 o3) (arrows o1 o2) (arrows o1 o3);
9 comp_assoc: ∀o1,o2,o3,o4. ∀a34,a23,a12.
10 comp o1 o3 o4 a34 (comp o1 o2 o3 a23 a12) = comp o1 o2 o4 (comp o2 o3 o4 a34 a23) a12;
11 id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o2) a = a;
12 id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a
15 notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
16 interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
17 interpretation "arrows" 'arrows A B = (unary_morphism A B).
19 notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
20 notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
22 interpretation "id" 'id A = (id ? A).
24 ndefinition SETOID : category.
27 ##| napply unary_morph_setoid;
28 ##| #o; @ (λx.x); #a; #b; #H; napply H;
29 ##| napply comp_binary_morphisms; (*CSC: why not ∘?*)
30 ##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
31 ##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
34 unification hint 0 ≔ ;
35 R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
36 (comp_assoc SETOID) (id_neutral_left SETOID)
37 (id_neutral_right SETOID))
38 (* -------------------------------------------------------------------- *) ⊢
41 unification hint 0 ≔ x,y ;
42 R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
43 (comp_assoc SETOID) (id_neutral_left SETOID)
44 (id_neutral_right SETOID))
45 (* -------------------------------------------------------------------- *) ⊢
46 arrows R x y ≡ unary_morph_setoid x y.
48 unification hint 0 ≔ A,B ;
49 T ≟ (unary_morph_setoid A B)
50 (* ----------------------------------- *) ⊢
51 unary_morphism A B ≡ carr T.
54 ndefinition TYPE : setoid1.
57 alias symbol "eq" = "setoid eq".
58 napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
59 ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
60 ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
61 ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
62 @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
63 ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
65 ##[ napply (.= (†(Hf …))); napply Hg;
66 ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##]
69 unification hint 0 ≔ ;
70 R ≟ (mk_setoid1 setoid (eq1 TYPE))
71 (* -------------------------------------------- *) ⊢
74 nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
76 prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
79 interpretation "prop01" 'prop1 c = (prop01 ????? c).