Mercurial > hg > Members > kono > Proof > category

changeset 873:0b5fb015009c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
join
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 09 Apr 2020 09:47:00 +0900
parents bfe0215593b9
children 484f19f16712
files CCCGraph1.agda
diffstat 1 files changed, 18 insertions(+), 100 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Thu Apr 09 07:54:18 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 09 09:47:00 2020 +0900
@@ -68,77 +68,32 @@
    refl-<r> refl = refl
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
-   id a ・ g = g
-   ○ a ・ g = ○ _
-   < f , g > ・  h = <  f ・ h  ,  g ・ h  >
-   iv f (id _) ・ h = iv f h 
-   iv π < g , g₁ > ・  h = g ・ h
-   iv π' < g , g₁ > ・  h = g₁ ・ h
-   iv ε < g , g₁ > ・  h = iv ε < g ・ h , g₁ ・ h >
-   iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > 
-   iv f ( (○ a)) ・ g = iv f ( ○ _ )
-   iv x y ・ id a = iv x y
-   iv f (iv f₁ g) ・ h with iv f₁ g ・ h 
-   (iv f (iv f₁ g) ・ h) | id a = iv f (id a)
-   (iv f (iv f₁ g) ・ h) | ○ a = iv f (○ a)
-   (iv π (iv f₁ g) ・ h) | < t , t₁ > = t
-   (iv π' (iv f₁ g) ・ h) | < t , t₁ > = t₁
-   (iv ε (iv f₁ g) ・ h) | < t , t₁ > = iv ε  < t , t₁ >
-   (iv (f *) (iv f₁ g) ・ h) | < t , t₁ > = iv (f *) < t , t₁ >
-   (iv f (iv f₁ g) ・ h) | iv f₂ t = iv f (iv f₂ t)
+   f ・ h with eval f
+   ... | id a = eval h
+   ... | ○ a = ○ _
+   ... | < f1 , g > = <  f1 ・ h  ,  g ・ h  >
+   ... | iv f1 (id _) = iv f1 h 
+   ... | iv π < g , g₁ > = ?
+   ... | iv π' < g , g₁ > = {!!} -- g₁ ・ h
+   ... | iv ε < g , g₁ > = {!!} -- iv ε < g ・ h , g₁ ・ h >
+   ... | iv (x *) < g , g₁ > = {!!} -- iv (x *) < g ・ h , g₁ ・ h > 
+   ... | iv x ( (○ a)) = iv x ( ○ _ )
+   ... | iv x f1 = {!!}
 
    _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
    _==_ {a} {b} x y   = eval x  ≡ eval  y 
 
    identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
-   identityR {a} {.a} {id a} = refl
-   identityR {a} {⊤} {○ a} = refl
-   identityR {_} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
-   identityR {_} {_} {iv f (id a)} = refl
-   identityR {_} {_} {iv f (○ a)} = refl
-   identityR {_} {_} {iv π < g , g₁ >} = identityR {_} {_} {g} 
-   identityR {_} {_} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} 
-   identityR {_} {_} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
-   identityR {_} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
-   identityR {_} {_} {iv f (iv g h)} = refl
+   identityR = {!!}
+
+   distr-e : {a b c : Objs } ( f : Arrows b c ) ( g : Arrows a b ) → eval ( f ・ g ) ≡ (eval f ・ eval g)
+   distr-e = {!!}
 
    open import Data.Empty 
    open import Relation.Nullary 
 
    open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)
 
-   std-iv : {a b c d : Objs} (x : Arrow c d) (y : Arrow b c ) (f : Arrows a b) 
-        →  ( {b1 b2 : Objs } → {g : Arrows a b1 } {h : Arrows a b2 } → ¬ (eval f) ≅ < g , h > )
-        → eval (iv x ( iv y f ) ) ≡ iv x ( eval (iv y f ) )
-   std-iv x y (id a) _ = refl
-   std-iv x y (○ a) _ = refl
-   std-iv x y < f , f₁ > ne = ⊥-elim (ne refl)
-   std-iv x y (iv z f) ne with eval (iv z f) 
-   std-iv x y (iv z f) ne | id a = refl
-   std-iv x y (iv z f) ne | ○ a = refl
-   std-iv x y (iv z f) ne | < t , t₁ > = ⊥-elim (ne refl)
-   std-iv (arrow x) _ (iv z f) ne | iv z1 t = refl
-   std-iv π y (iv z f) ne | iv z1 t = refl
-   std-iv π' y (iv z f) ne | iv z1 t = refl
-   std-iv ε y (iv z f) ne | iv z1 t = refl
-   std-iv (x *) y (iv z f) ne | iv z1 t = refl
-
-   std-iv' : {a b c : Objs}  (y : Arrow b c ) (f : Arrows a b) 
-        →  ( {b1 b2 : Objs } → {g : Arrows a b1 } {h : Arrows a b2 } → ¬ (eval f) ≅ < g , h > )
-        → eval ( iv y f )  ≡  iv y (eval f ) 
-   std-iv' y (id a) ne = refl
-   std-iv' y (○ a) ne = refl
-   std-iv' y < f , f₁ > ne = ⊥-elim (ne refl)
-   std-iv' y (iv f z) ne with eval (iv f z)  
-   std-iv' y (iv f z) ne | id a = refl
-   std-iv' y (iv f z) ne | ○ a = refl
-   std-iv' y (iv f z) ne | < t , t₁ > = ⊥-elim (ne refl)
-   std-iv' (arrow x) (iv f z) ne | iv f₁ t = refl
-   std-iv' π (iv f z) ne | iv f₁ t = refl
-   std-iv' π' (iv f z) ne | iv f₁ t = refl
-   std-iv' ε (iv f z) ne | iv f₁ t = refl
-   std-iv' (y *) (iv f z) ne | iv f₁ t = refl
-
    idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
    idem-eval (id a) = refl
    idem-eval (○ a) = refl
@@ -162,17 +117,7 @@
    --   lemma =  std-iv f f₁ t {!!}
 
    assoc-iv : {a b c d : Objs} (x : Arrow c d) (f : Arrows b c) (g : Arrows a b ) → eval (iv x (f ・ g)) ≡ eval (iv x f ・ g)
-   assoc-iv x (id a) g = refl
-   assoc-iv x (○ a) g = refl
-   assoc-iv π < f , f₁ > g = refl
-   assoc-iv π' < f , f₁ > g = refl
-   assoc-iv ε < f , f₁ > g = refl
-   assoc-iv (x *) < f , f₁ > g = refl
-   assoc-iv x (iv f g) h = begin
-            eval (iv x (iv f g ・ h)) 
-        ≡⟨ {!!} ⟩
-            eval (iv x (iv f g) ・ h)
-        ∎  where open ≡-Reasoning
+   assoc-iv = {!!}
 
 
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
@@ -194,37 +139,10 @@
                }
            }  where
                identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) == f
-               identityL {_} {_} {id a} = refl
-               identityL {_} {_} {○ a} = refl
-               identityL {a} {b} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityL {_} {_} {f}) (identityL {_} {_} {f₁})
-               identityL {_} {_} {iv f f₁} = refl
+               identityL = {!!}
                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 (○ a) g h = refl
-               associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
-               associative {a} (iv π < f , f1 > ) g h = associative f g h
-               associative {a} (iv π' < f , f1 > ) g h = associative f1 g h
-               associative {a} (iv ε < f , f1 > ) g h = cong ( λ k → iv ε k ) ( associative  < f , f1 >  g h )
-               associative {a} (iv (x *) < f , f1 > ) g h = cong ( λ k → iv (x *) k ) ( associative  < f , f1 >  g h )
-               associative {a} (iv x (id _)) g h =  begin
-                       eval (iv x (id _) ・ (g ・ h))
-                    ≡⟨⟩
-                       eval (iv x (g ・ h))
-                    ≡⟨ assoc-iv x g h ⟩
-                       eval (iv x g ・ h)
-                    ≡⟨⟩
-                       eval ((iv x (id _) ・ g) ・ h)
-                    ∎  where open ≡-Reasoning
-               associative {a} (iv x (○ _)) g h =  refl
-               associative {a} (iv x (iv y f)) g h = begin
-                       eval (iv x (iv y f) ・ (g ・ h))
-                    ≡⟨ sym (assoc-iv x (iv y f) ( g ・ h)) ⟩
-                       eval (iv x ((iv y f) ・ (g ・ h)))
-                    ≡⟨ {!!}  ⟩
-                       eval ((iv x (iv y f) ・ g) ・ h)
-                    ∎  where open ≡-Reasoning
-                  -- cong ( λ k → iv x k ) (associative f g h) 
+               associative = {!!}
                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 = {!!}