Mercurial > hg > Members > kono > Proof > category

changeset 839:111ee96c09ab

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 09:15:52 +0900
parents be4b8e70fa8e
children f9167bc017cd
files CCCGraph1.agda
diffstat 1 files changed, 9 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Thu Apr 02 08:43:50 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 09:15:52 2020 +0900
@@ -32,10 +32,10 @@
       iv  : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c   -- cas iv
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
-   _・_ {a} {b} {⊤} _ _ = iv (○ a) (id a)
    id a ・ g = g
    < f , g > ・  h = <  f ・ h  ,  g ・ h  >
    iv f (id _) ・ h = iv f h
+   iv (○ a) g ・  h = iv (○ _) (id _)
    iv π < g , g₁ > ・  h = g ・ h
    iv π' < g , g₁ > ・  h = g₁ ・ h
    iv ε < g , g₁ > ・  h = iv ε < g ・ h , g₁ ・ h >
@@ -58,19 +58,19 @@
                }
            }  where
                identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
-               identityL {_} {_} {id a} = {!!}
-               identityL {a} {b} {< f , f₁ >} = {!!}
-               identityL {_} {_} {iv 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} {_} {id a} = {!!}
-               identityR {a} {b} {< f , g >} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
+               identityR {a} {_} {id a} = refl
+               identityR {a} {b} {< f , g >} = cong₂ ( λ j k → < j , k > ) ( identityR {_} {_} {f} ) ( identityR {_} {_} {g} )
                identityR {a} {b} {iv x 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
                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 = {!!}
-               associative (< f , f1 > ) g h = {!!}
-               associative (iv x f) g h = {!!} -- cong ( λ k → iv x k ) ( associative 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 )