Mercurial > hg > Members > kono > Proof > category

changeset 843:a73acfdef643

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 13:43:43 +0900
parents fa9d5d2b965d
children 3b8c1ca0d737
files CCCGraph1.agda
diffstat 1 files changed, 20 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Thu Apr 02 12:11:22 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 13:43:43 2020 +0900
@@ -65,22 +65,30 @@
                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} {.a} {id a} = refl
+               identityR≡ {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR≡ {a} {_} {f} ) (identityR≡ {a} {_} {f₁} )
+               identityR≡ {a} {b} {iv x (id a)} = refl
+               identityR≡ {a} {b} {iv π < f , f₁ >} = {!!}
+               identityR≡ {a} {b} {iv π' < f , f₁ >} = {!!}
+               identityR≡ {a} {⊤} {iv (○ .(_ ∧ _)) < f , f₁ >} = {!!}
+               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 {a} {c} {d} x (iv {a} {d} {c1} f f₁)} = begin -- cong ( λ k → iv x k ・ id a ) {!!} -- ( identityR {_} {_} {iv f f₁} )
+                       iv x (iv f f₁) ・ id a
+                    ≡⟨ {!!} ⟩
+                       iv x ((iv f f₁) ・ id a)
+                    ≡⟨ cong (λ k → iv x k) identityR≡ ⟩
+                       iv x (iv f f₁) 
+                    ∎  where open ≡-Reasoning
                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 (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₁ >} = 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 = {!!}
+               identityR = {!!}
                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 = 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 )
 
+               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 = {!!}