Mercurial > hg > Members > kono > Proof > category

changeset 840:f9167bc017cd

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:33:08 +0900
parents 111ee96c09ab
children 9fa1bf29fbf4
files CCCGraph1.agda
diffstat 1 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Thu Apr 02 09:15:52 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 09:33:08 2020 +0900
@@ -64,7 +64,10 @@
                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} {iv x f} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
+               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 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
@@ -72,5 +75,5 @@
                             (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 )
+               associative (iv x f) g h = {!!} -- cong ( λ k → iv x k ) ( associative f g h )