Mercurial > hg > Members > kono > Proof > category

changeset 845:0c81ded4a734

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Apr 2020 20:55:29 +0900
parents 3b8c1ca0d737
children 4013cbfdd15e
files CCCGraph1.agda
diffstat 1 files changed, 22 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Thu Apr 02 20:42:18 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 20:55:29 2020 +0900
@@ -44,8 +44,20 @@
    iv f ( (○ a)) ・ g = iv f ( ○ _ )
    iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )
 
+   eval :  {a b  : Objs } (f : Arrows a b ) → Arrows a b
+   eval ( id a ) = id a
+   eval ( ○ a ) = ○ a
+   eval ( < f , g > ) = <  eval f   , eval g   >
+   eval ( iv f (id _) ) = iv f (id _)
+   eval ( iv π < g , g₁ > ) = eval g 
+   eval ( iv π' < g , g₁ > ) = eval g₁ 
+   eval ( iv ε < g , g₁ > ) = iv ε < eval g  , eval g₁  >
+   eval ( iv (f *) < g , g₁ > ) = iv (f *) < eval g  , eval g₁  > 
+   eval ( iv f ( (○ a)) ) = iv f ( ○ _ )
+   eval ( iv f (iv f₁ g) ) = iv f ( iv f₁ (eval g))
+
    _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
-   _==_ {a} {b} x y   = ( x ・ id a ) ≡ ( y ・ id a )
+   _==_ {a} {b} x y   = eval x  ≡ eval y 
 
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
@@ -79,7 +91,7 @@
                identityR≡ {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR≡ {a} {_} {f} ) (identityR≡ {a} {_} {f₁} )
                identityR≡ {a} {b} {iv x (id a)} = refl
                identityR≡ {a} {b} {iv x (○ a)} = refl
-               identityR≡ {a} {b} {iv π < f , f₁ >} = ?
+               identityR≡ {a} {b} {iv π < f , f₁ >} = {!!}
                identityR≡ {a} {b} {iv π' < f , f₁ >} = {!!}
                identityR≡ {a} {b} {iv ε < f , f₁ >} = cong ( λ k → iv ε k ) ( identityR≡ {_} {_} {< f , f₁ >} )
                identityR≡ {a} {_} {iv (x *) < f , f₁ >} = cong ( λ k → iv (x *) k ) ( identityR≡ {_} {_} {< f , f₁ >} )
@@ -91,7 +103,14 @@
                        iv x (iv f f₁) 
                     ∎  where open ≡-Reasoning
                identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
-               identityR = {!!}
+               identityR {a} {.a} {id a} = refl
+               identityR {a} {.⊤} {○ a} = refl
+               identityR {a} {.(_ ∧ _)} {< f , f₁ >} = cong₂ ( λ j k → < j , k > ) ( identityR {_} {_} {f} ) ( identityR {_} {_} {f₁} )
+               identityR {a} {.(atom _)} {iv (arrow x) f₁} = {!!}
+               identityR {a} {b} {iv π f₁} = {!!}
+               identityR {a} {b} {iv π' f₁} = {!!}
+               identityR {a} {b} {iv ε f₁} = {!!}
+               identityR {a} {.(_ <= _)} {iv (f *) f₁} = ?
                associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
                             (f ・ (g ・ h)) == ((f ・ g) ・ h)
                associative (id a) g h = refl