Mercurial > hg > Members > kono > Proof > category
changeset 842:fa9d5d2b965d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Apr 2020 12:11:22 +0900 |
| parents | 9fa1bf29fbf4 |
| children | a73acfdef643 |
| files | CCCGraph1.agda |
| diffstat | 1 files changed, 7 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph1.agda Thu Apr 02 11:52:07 2020 +0900 +++ b/CCCGraph1.agda Thu Apr 02 12:11:22 2020 +0900 @@ -55,9 +55,9 @@ Id = λ{a} → id a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; - identityL = identityL ; - identityR = identityR ; - o-resp-≈ = o-resp-≈ ; + identityL = λ {a b f} → identityL {a} {b} {f} ; + identityR = λ {a b f} → identityR {a} {b} {f} ; + o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = λ{a b c d f g h } → associative f g h } } where @@ -71,10 +71,10 @@ identityR {a} {b} {iv x (id a)} = refl identityR {a} {b} {iv π < f , f₁ >} = identityR {a} {b} {f} identityR {a} {b} {iv π' < f , f₁ >} = identityR {a} {b} {f₁} - identityR {a} {.⊤} {iv (○ .(_ ∧ _)) < f , f₁ >} = refl - identityR {a} {b} {iv ε < f , f₁ >} = {!!} - identityR {a} {.(_ <= _)} {iv (x *) < f , f₁ >} = {!!} - identityR {a} {b} {iv x (iv f f₁)} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} ) + identityR {a} {⊤} {iv (○ .(_ ∧ _)) < f , f₁ >} = refl + 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₁ >} ) + identityR {a} {b} {iv x (iv f f₁)} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {iv f 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-≈ f=g h=i = {!!}