Mercurial > hg > Members > kono > Proof > category

changeset 848:18bbd9e31c48

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 Fri, 03 Apr 2020 18:44:15 +0900
parents f2729064016d
children 3b7b8e510047
files CCCGraph1.agda
diffstat 1 files changed, 10 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Fri Apr 03 17:50:48 2020 +0900
+++ b/CCCGraph1.agda	Fri Apr 03 18:44:15 2020 +0900
@@ -62,6 +62,16 @@
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
    ==←≡ eq = cong (λ k → k ・ id _) eq
 
+   assoc-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → iv x f ・ g ≡ iv x ( f ・ g )
+   assoc-iv x f (id _) = {!!}
+   assoc-iv x (id a) g = {!!}
+   assoc-iv x (○ a) g = {!!}
+   assoc-iv π < f , f₁ > g = {!!}
+   assoc-iv π' < f , f₁ > g = {!!}
+   assoc-iv ε < f , f₁ > g = {!!}
+   assoc-iv (x *) < f , f₁ > g = {!!}
+   assoc-iv x (iv f f₁) g = {!!}
+
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
             Obj  = Objs;
@@ -82,23 +92,6 @@
                identityL {_} {_} {○ a} = refl
                identityL {a} {b} {< f , f₁ >} = refl
                identityL {_} {_} {iv f f₁} = refl
-               assoc-iv1 : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → (iv x f ・ g) == (iv x ( f ・ g ))
-               assoc-iv1 (arrow x) f g = ?
-               assoc-iv1 π f g = {!!}
-               assoc-iv1 π' f g = {!!}
-               assoc-iv1 ε f g = {!!}
-               assoc-iv1 (x *) f g = {!!}
-               assoc-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → iv x f ・ g ≡ iv x ( f ・ g )
-               assoc-iv (arrow x) (id .(atom _)) g = {!!}
-               assoc-iv (arrow x) (iv f f₁) g = {!!}
-               assoc-iv π (id .(_ ∧ _)) g = {!!}
-               assoc-iv π < f , f₁ > g = {!!}
-               assoc-iv π (iv f f₁) g = {!!}
-               assoc-iv π' f g = {!!}
-               assoc-iv ε (id .((_ <= _) ∧ _)) g = {!!}
-               assoc-iv ε < f , f₁ > g = {!!}
-               assoc-iv ε (iv f f₁) g = {!!}
-               assoc-iv (x *) f g = {!!}
                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