Mercurial > hg > Members > kono > Proof > category

changeset 10:3ef6a17353d1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reasoning
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2013 18:45:48 +0900
parents 3207ae6d4442
children 2cbecadc56c1
files nat.agda
diffstat 1 files changed, 12 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Sun Jul 07 18:16:46 2013 +0900
+++ b/nat.agda	Sun Jul 07 18:45:48 2013 +0900
@@ -127,27 +127,26 @@
                       ( Hom A b ( FObj T c )) -> (  Hom A a ( FObj T b)) -> Hom A a ( FObj T c )
      join c g f = A [ Trans μ c  o A [ FMap T g  o f ] ]
 
-open import Relation.Binary  renaming (Trans to Trans1 )
+
 open import Relation.Binary.Core  renaming (Trans to Trans1 )
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
-module ≈-Reasoning where
+module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
 
   -- The code in Relation.Binary.EqReasoning cannot handle                                                                              
   -- heterogeneous equalities, hence the code duplication here.                                                                         
 
-  refl-hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } 
+  refl-hom :   {a b : Obj A } 
                 { x y z : Hom A a b }  →
         A [ x ≈ x ]
-  refl-hom = \a -> IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory a ))
+  refl-hom =  IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
 
-  trans-hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj 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 c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory a ))) b c
+  trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c
 
-  infixr  2 _∎_
-  infixr 2 _≈⟨_!_⟩_ 
+  infixr  2 _∎
+  infixr 2 _≈⟨_⟩_ 
   infix  1 begin_
 
   data IsRelatedTo  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } ( x y : Hom A a b ) :
@@ -158,13 +157,13 @@
            IsRelatedTo A x y → A [ x ≈ y ]
   begin relTo x≈y = x≈y
 
-  _≈⟨_!_⟩_ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->  {a b : Obj A }
+  _≈⟨_⟩_ :   {a b : Obj A }
                 ( x : Hom A a b ) → { y z : Hom A a b } → 
                 A [ x ≈ y ] → IsRelatedTo A y z → IsRelatedTo A x z
-  a ≈⟨ _ !  x≈y ⟩ relTo y≈z  = relTo ( trans-hom a x≈y y≈z )
+  a ≈⟨ x≈y ⟩ relTo y≈z  = relTo ( trans-hom x≈y y≈z )
 
-  _∎_ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
-  a ∎ _ = relTo ( refl-hom a )
+  _∎ :   {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
+  _ ∎  = relTo ( refl-hom )
 
 open Kleisli
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
@@ -179,8 +178,6 @@
 Lemma7 c k = {!!}
 
 
-
-
 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }