-(**************************************************************************)
-(* ___ *)
-(* ||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 "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. unary_morphism (arrows o1 o2) (unary_morph_setoid (arrows o2 o3) (arrows o1 o3));
+ 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;
@;
##[ napply setoid;
##| napply unary_morph_setoid;
-##| #o; @ (λx.x); //
-##| #o1; #o2; #o3; napply mk_binary_morphism [ #f; #g; @(λx.g (f x)) ]
- nnormalize; /3/
-##| nnormalize; /4/
-##|##6,7: nnormalize; /2/ ]
+##| #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 ≔ ;
(* ----------------------------------- *) ⊢
unary_morphism A B ≡ carr T.
-(*
ndefinition TYPE : setoid1.
@ setoid; @;
interpretation "new I" 'I a = (nI ? a).
ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
-
+(*
nlemma elim_eq_TYPE : ∀A,B:setoid.∀P:CProp[1]. A=B → ((B ⇒ A) → P) → P.
#A; #B; #P; *; #f; *; #g; #_; #IH; napply IH; napply g;
nqed.
##[ @(f e);
*)
-(*
ndefinition image_is_ext : ∀A:nAx.∀a:A.∀i:𝐈 a.𝛀^A.
#A; #a; #i; @ (image … i); #x; #y; #H; @;
##[ *; #d; #Ex; @ d; napply (.= H^-1); nassumption;
@ (f i); #a; #Ha; napply H1;
ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]);
- ##[##2: #E; napply (. (#‡E^-1)); napply Ha; ##]
+ ##[##2: #E; alias symbol "refl" = "refl".
+ alias symbol "prop2" = "prop21 mem".
+ alias symbol "invert" = "setoid1 symmetry".
+ napply (. (#‡E^-1)); napply Ha; ##]
@; #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