Mercurial > hg > Members > kono > Proof > category
changeset 884:93dd4c041969
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 Apr 2020 22:06:02 +0900 |
| parents | 0173a5dc6a42 |
| children | a502754b890a |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 10 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Sat Apr 11 20:32:37 2020 +0900 +++ b/CCCGraph1.agda Sat Apr 11 22:06:02 2020 +0900 @@ -234,12 +234,18 @@ d-eval (○ a) g = refl d-eval < f , f₁ > g = cong₂ (λ j k → < j , k > ) (d-eval f g) (d-eval f₁ g) d-eval (iv x (id a)) g = iv-d x g - d-eval (iv (x *) (○ a)) g = {!!} + d-eval (iv (x *) (○ a)) g = refl d-eval (iv π < f , f₁ >) g = d-eval f g d-eval (iv π' < f , f₁ >) g = d-eval f₁ g - d-eval (iv ε < f , f₁ >) g = {!!} - d-eval (iv (x *) < f , f₁ >) g = {!!} - d-eval (iv x (iv f f₁)) g = {!!} + d-eval (iv ε < f , f₁ >) g = cong₂ (λ j k → iv ε k ) (d-eval f g) ( + cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g )) + d-eval (iv (x *) < f , f₁ >) g = cong₂ (λ j k → iv (x *) k ) (d-eval f g) ( + cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g )) + d-eval (iv x (iv f f₁)) g = begin + eval (iv x (iv f f₁) ・ g) + ≡⟨ {!!} ⟩ + eval (eval (iv x (iv f f₁)) ・ eval g) + ∎ where open ≡-Reasoning ore : {A B C : Objs} (f g : Arrows A B) (h i : Arrows B C) → eval f ≡ eval g → eval h ≡ eval i → eval (h ・ f) ≡ eval (i ・ g) ore f g h i f=g h=i = begin