Mercurial > hg > Members > kono > Proof > category

changeset 881:da0a1dd0c2ee

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 Sat, 11 Apr 2020 17:29:45 +0900
parents 543ceeb10191
children 6c69d48e6015
files CCCGraph1.agda
diffstat 1 files changed, 11 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Sat Apr 11 12:07:45 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 11 17:29:45 2020 +0900
@@ -134,13 +134,21 @@
                }
            }  where 
               iv-e : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ iv x (eval g)
-              iv-e = ?
+              iv-e = {!!}
+              iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c  ) ( g : Arrows a (atom b) )
+                   → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g)
+              iv-e-arrow x (id (atom _)) = refl
+              iv-e-arrow x (iv f g) with eval (iv f g) 
+              iv-e-arrow x (iv f g) | id (atom _) = refl
+              iv-e-arrow x (iv f g) | iv f₁ t = refl
               iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g))
               iv-d (arrow x) g = begin
                   eval (iv (arrow x) g) 
-                ≡⟨ {!!} ⟩
+                ≡⟨ iv-e-arrow x g ⟩
                   iv (arrow x) (eval g)
-                ≡⟨ {!!} ⟩
+                ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩
+                  iv (arrow x) (eval (eval g))
+                ≡⟨ sym (iv-e-arrow x (eval g)) ⟩
                   eval (iv (arrow x) (eval g))
                 ∎  where open ≡-Reasoning
               iv-d π (id _) = refl