Mercurial > hg > Members > kono > Proof > category

changeset 29:87cefecc5663

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
notation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 Jul 2013 11:46:58 +0900
parents 5289c46d8eef
children 98b8431a419b
files nat.agda
diffstat 1 files changed, 24 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sat Jul 13 03:05:43 2013 +0900
+++ b/nat.agda	Sat Jul 13 11:46:58 2013 +0900
@@ -133,71 +133,75 @@
 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
   open import Relation.Binary.Core renaming ( Trans to Trasn1 )
 
-  refl-hom :   {a b : Obj A } { x : Hom A a b }  →
-        A [ x ≈ x ]
+  _o_ :  {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b
+  x o y = A [ x o y ]
+
+  _≈_ :  {a b : Obj A }   → Rel (Hom A a b) ℓ
+  x ≈ y = A [ x ≈ y ]
+
+  infixr 9 _o_
+  infix  4 _≈_
+
+  refl-hom :   {a b : Obj A } { x : Hom A a b }  →  x ≈ x 
   refl-hom =  IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
 
-  trans-hom :   {a b : Obj A } 
-                { x y z : Hom A a b }  →
-        A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ]
+  trans-hom :   {a b : Obj A } { x y z : Hom A a b }  →
+         x ≈ y →  y ≈ z  →  x ≈ z 
   trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c
 
   -- some short cuts
 
   car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
-         A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y  o f ] ]
+          x ≈ y  → ( x o f ) ≈ ( y  o f )
   car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
 
   cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
-         A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f  o y ] ]
+          x ≈ y  →  f o x  ≈  f  o y 
   cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 
 
   id :  (a  : Obj A ) →  Hom A a a
   id a =  (Id {_} {_} {_} {A} a) 
 
-  idL :  {a b : Obj A } { f : Hom A b a } → A [ A [ id a o f ] ≈ f ]
+  idL :  {a b : Obj A } { f : Hom A b a } →  id a o f  ≈ f 
   idL =  IsCategory.identityL (Category.isCategory A)
 
-  idR :  {a b : Obj A } { f : Hom A a b } → A [ A [ f o id a ] ≈ f ]
+  idR :  {a b : Obj A } { f : Hom A a b } →  f o id a  ≈ f 
   idR =  IsCategory.identityR (Category.isCategory A)
 
-  sym :  {a b : Obj A } { f g : Hom A a b } -> A [ f ≈ g ] -> A [ g ≈ f ]
+  sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
   sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
 
   assoc :   {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
-                                  → A [ A [ f o A [ g o h ] ]  ≈ A [ A [ f o g ] o h ] ]
+                                  →  f o ( g o h )  ≈ ( f o g ) o h
   assoc =  IsCategory.associative (Category.isCategory A)
 
   distr :  (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
-     → A [ ( FMap T (A [ g o f ] ))  ≈ (A [ FMap T g o FMap T f ]) ]
+     →   FMap T ( g o f  )  ≈  FMap T g o FMap T f 
   distr T = IsFunctor.distr ( isFunctor T )
 
   nat : { c₁′ c₂′ ℓ′ : Level}  (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b}  {F G : Functor D A }
       →  (η : NTrans D A F G )
-      → A [ A [ (  FMap G f ) o  ( Trans η a ) ]  ≈ A [ (Trans η b ) o  (FMap F f)  ] ]
+      →   FMap G f  o  Trans η a   ≈ Trans η b  o  FMap F f
   nat _ η  =  IsNTrans.naturality ( isNTrans η  )
 
-  _o_ :  {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) -> Hom A c b
-  x o y = A [ x o y ]
-
   infixr  2 _∎
   infixr 2 _≈⟨_⟩_ 
   infix  1 begin_
 
 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
---  ≈-to-≡ : {a b : Obj A } { x y : Hom A a b }  -> A [ x ≈  y ] -> x ≡ y
+--  ≈-to-≡ : {a b : Obj A } { x y : Hom A a b }  → A [ x ≈  y ] → x ≡ y
 --  ≈-to-≡ refl-hom = refl
 
   data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
                      Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
-    relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y
+    relTo : (x≈y : x ≈ y ) → x IsRelatedTo y
 
   begin_ : { a b : Obj A } { x y : Hom A a b } →
-           x IsRelatedTo y → A [ x ≈ y ]
+           x IsRelatedTo y → x ≈ y 
   begin relTo x≈y = x≈y
 
   _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 
-           A [ x ≈ y ] → y IsRelatedTo z → x IsRelatedTo z
+           x ≈ y → y IsRelatedTo z → x IsRelatedTo z
   _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
 
   _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x