--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "logic/pts.ma".
+
+ndefinition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x.
+ndefinition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x.
+ndefinition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y.
+
+nrecord equivalence_relation2 (A:Type[2]) : Type[3] ≝
+ { eq_rel2:2> A → A → CProp[2];
+ refl2: reflexive2 ? eq_rel2;
+ sym2: symmetric2 ? eq_rel2;
+ trans2: transitive2 ? eq_rel2
+ }.
--- /dev/null
+
+include "sets/sets.ma".
+
+ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
+#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
+##[ #f; #g; napply (∀x,y. f x y = g x y);
+##| #f; #x; #y; napply #;
+##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
+##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+
+ndefinition unary_morph_setoid : setoid → setoid → setoid.
+#S1; #S2; @ (unary_morphism S1 S2); @;
+##[ #f; #g; napply (∀x. f x = g x);
+##| #f; #x; napply #;
+##| #f; #g; #H; #x; napply ((H x)^-1);
+##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+
+nrecord category : Type[2] ≝
+ { objs:> Type[1];
+ arrows: objs → objs → setoid;
+ id: ∀o:objs. arrows o o;
+ comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
+ comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
+ comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
+ id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
+ id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
+ }.
+
+notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
+interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
+interpretation "arrows" 'arrows A B = (unary_morphism A B).
+
+notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
+notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
+
+interpretation "id" 'id A = (id ? A).
+
+ndefinition SETOID : category.
+@;
+##[ napply setoid;
+##| napply unary_morph_setoid;
+##| #o; @ (λx.x); #a; #b; #H; napply H;
+##| #o1; #o2; #o3; @;
+ ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
+ ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x)));
+ napply (.= (†(H1 x))); napply #; ##]
+##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
+##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
+nqed.
+
+unification hint 0 ≔ ;
+ R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
+ (comp_assoc SETOID) (id_neutral_left SETOID)
+ (id_neutral_right SETOID))
+ (* -------------------------------------------------------------------- *) ⊢
+ objs R ≡ setoid.
+
+ unification hint 0 ≔ x,y ;
+ R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
+ (comp_assoc SETOID) (id_neutral_left SETOID)
+ (id_neutral_right SETOID))
+ (* -------------------------------------------------------------------- *) ⊢
+ arrows R x y ≡ unary_morph_setoid x y.
+
+unification hint 0 ≔ A,B ;
+ T ≟ (unary_morph_setoid A B)
+ (* ----------------------------------- *) ⊢
+ unary_morphism A B ≡ carr T.
+
+
+ndefinition TYPE : setoid1.
+@ setoid; @;
+##[ #T1; #T2;
+ alias symbol "eq" = "setoid eq".
+ napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
+##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
+##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
+##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
+ @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
+ ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
+ @; #x;
+ ##[ napply (.= (†(Hf …))); napply Hg;
+ ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##]
+nqed.
+
+unification hint 0 ≔ ;
+ R ≟ (mk_setoid1 setoid (eq1 TYPE))
+ (* -------------------------------------------- *) ⊢
+ carr1 R ≡ setoid.
+
+nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
+ { fun01:1> A → B;
+ prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
+ }.
+
+interpretation "prop01" 'prop1 c = (prop01 ????? c).
--- /dev/null
+
+include "sets/sets.ma".
+include "sets/setoids2.ma".
+include "sets/categories.ma".
+
+(*
+ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
+#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
+##[ #f; #g; napply (∀x,y. f x y = g x y);
+##| #f; #x; #y; napply #;
+##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
+##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+
+ndefinition unary_morph_setoid : setoid → setoid → setoid.
+#S1; #S2; @ (unary_morphism S1 S2); @;
+##[ #f; #g; napply (∀x. f x = g x);
+##| #f; #x; napply #;
+##| #f; #g; #H; #x; napply ((H x)^-1);
+##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+
+nrecord category : Type[2] ≝
+ { objs:> Type[1];
+ arrows: objs → objs → setoid;
+ id: ∀o:objs. arrows o o;
+ comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
+ comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
+ comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
+ id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
+ id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
+ }.
+*)
+
+notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
+interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
+interpretation "arrows" 'arrows A B = (unary_morphism A B).
+
+(*
+notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
+notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
+
+interpretation "id" 'id A = (id ? A).
+
+ndefinition SETOID : category.
+@;
+##[ napply setoid;
+##| napply unary_morph_setoid;
+##| #o; @ (λx.x); #a; #b; #H; napply H;
+##| #o1; #o2; #o3; @;
+ ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
+ ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x)));
+ napply (.= (†(H1 x))); napply #; ##]
+##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #;
+##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##]
+nqed.
+
+unification hint 0 ≔ ;
+ R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
+ (comp_assoc SETOID) (id_neutral_left SETOID)
+ (id_neutral_right SETOID))
+ (* -------------------------------------------------------------------- *) ⊢
+ objs R ≡ setoid.
+
+ unification hint 0 ≔ x,y ;
+ R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID)
+ (comp_assoc SETOID) (id_neutral_left SETOID)
+ (id_neutral_right SETOID))
+ (* -------------------------------------------------------------------- *) ⊢
+ arrows R x y ≡ unary_morph_setoid x y.
+
+unification hint 0 ≔ A,B ;
+ T ≟ (unary_morph_setoid A B)
+ (* ----------------------------------- *) ⊢
+ unary_morphism A B ≡ carr T.
+
+
+ndefinition TYPE : setoid1.
+@ setoid; @;
+##[ #T1; #T2;
+ alias symbol "eq" = "setoid eq".
+ napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
+##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
+##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
+##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
+ @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #;
+ ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##]
+ @; #x;
+ ##[ napply (.= (†(Hf …))); napply Hg;
+ ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##]
+nqed.
+
+unification hint 0 ≔ ;
+ R ≟ (mk_setoid1 setoid (eq1 TYPE))
+ (* -------------------------------------------- *) ⊢
+ carr1 R ≡ setoid.
+
+nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
+ { fun01:1> A → B;
+ prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
+ }.
+
+interpretation "prop01" 'prop1 c = (prop01 ????? c).
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "properties/relations2.ma".
+include "sets/setoids1.ma".
+
+nrecord setoid2: Type[3] ≝
+ { carr2:> Type[2];
+ eq2: equivalence_relation2 carr2
+ }.
+
+ndefinition setoid2_of_setoid1: setoid1 → setoid2.
+ #s; @ (carr1 s); @ (carr1 s) (eq1 ?)
+ [ napply refl1
+ | napply sym1
+ | napply trans1]
+nqed.
+
+(*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
+ on _s: setoid to setoid1.*)
+(*prefer coercion Type_OF_setoid.*)
+
+interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y).
+interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+
+(*
+notation > "hvbox(a break =_12 b)" non associative with precedence 45
+for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
+*)
+notation > "hvbox(a break =_0 b)" non associative with precedence 45
+for @{ eq_rel ? (eq ?) $a $b }.
+notation > "hvbox(a break =_1 b)" non associative with precedence 45
+for @{ eq_rel1 ? (eq1 ?) $a $b }.
+notation > "hvbox(a break =_2 b)" non associative with precedence 45
+for @{ eq_rel2 ? (eq2 ?) $a $b }.
+
+interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r).
+interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans2" 'trans r = (trans2 ????? r).
+interpretation "trans1" 'trans r = (trans1 ????? r).
+interpretation "trans" 'trans r = (trans ????? r).
+
+nrecord unary_morphism2 (A,B: setoid2) : Type[2] ≝
+ { fun12:1> A → B;
+ prop12: ∀a,a'. eq2 ? a a' → eq2 ? (fun12 a) (fun12 a')
+ }.
+
+nrecord binary_morphism2 (A,B,C:setoid2) : Type[2] ≝
+ { fun22:2> A → B → C;
+ prop22: ∀a,a',b,b'. eq2 ? a a' → eq2 ? b b' → eq2 ? (fun22 a b) (fun22 a' b')
+ }.
+
+interpretation "prop12" 'prop1 c = (prop12 ????? c).
+interpretation "prop22" 'prop2 l r = (prop22 ???????? l r).
+interpretation "refl2" 'refl = (refl2 ???).
@; #w; #Hw; nwhd;
ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);
-
+(*
notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
[1]: http://upsilon.cc/~zack/research/publications/notation.pdf
D*)
+*)
\ No newline at end of file
projects / helm.git / commitdiff