Mercurial > hg > Members > kono > Proof > category

changeset 841:9fa1bf29fbf4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix ==
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Apr 2020 11:52:07 +0900
parents f9167bc017cd
children fa9d5d2b965d
files CCCGraph1.agda
diffstat 1 files changed, 18 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Thu Apr 02 09:33:08 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 11:52:07 2020 +0900
@@ -10,6 +10,7 @@
 
 module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
    open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+   open import  Relation.Binary.Core 
    open Graph
    
    data Objs : Set (c₁ ⊔ c₂) where
@@ -42,37 +43,43 @@
    iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > 
    iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )
 
+   _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
+   _==_ {a} {b} x y   = ( x ・ id a ) ≡ ( y ・ id a )
+
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
             _o_ =  λ{a} {b} {c} x y → x ・ y ;
-            _≈_ =  λ x y → x  ≡ y ;
+            _≈_ =  λ x y → x  == y ;
             Id  =  λ{a} → id a ;
             isCategory  = record {
                     isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-                    identityL  = identityL; 
+                    identityL  = identityL ; 
                     identityR  = identityR ; 
-                    o-resp-≈  = o-resp-≈  ; 
+                    o-resp-≈  = o-resp-≈ ; 
                     associative  = λ{a b c d f g h } → associative  f g h
                }
            }  where
-               identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
+               identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) == f
                identityL {_} {_} {id a} = refl
                identityL {a} {b} {< f , f₁ >} = refl
                identityL {_} {_} {iv f f₁} = refl
-               identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
+               identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
                identityR {a} {_} {id a} = refl
-               identityR {a} {b} {< f , g >} = cong₂ ( λ j k → < j , k > ) ( identityR {_} {_} {f} ) ( identityR {_} {_} {g} )
+               identityR {a} {b} {< f , g >} =  cong₂ ( λ j k → < j , k > ) (  identityR {_} {_} {f} ) ( identityR {_} {_} {g} ) 
                identityR {a} {b} {iv x (id a)} = refl
-               identityR {a} {b} {iv π < f , f₁ >} = {!!}
-               identityR {a} {b} {iv x < f , f₁ >} = {!!}
+               identityR {a} {b} {iv π < f , f₁ >} = identityR {a} {b} {f}
+               identityR {a} {b} {iv π' < f , f₁ >} = identityR {a} {b} {f₁}
+               identityR {a} {.⊤} {iv (○ .(_ ∧ _)) < f , f₁ >} = refl
+               identityR {a} {b} {iv ε < f , f₁ >} = {!!}
+               identityR {a} {.(_ <= _)} {iv (x *) < f , f₁ >} = {!!}
                identityR {a} {b} {iv x (iv f f₁)} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
                o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
-                            f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
-               o-resp-≈  refl refl = refl
+                            f == g → h == i → (h ・ f) == (i ・ g)
+               o-resp-≈  f=g h=i = {!!}
                associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
-                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
+                            (f ・ (g ・ h)) == ((f ・ g) ・ h)
                associative (id a) g h = refl
                associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
                associative (iv x f) g h = {!!} -- cong ( λ k → iv x k ) ( associative f g h )