Mercurial > hg > Members > kono > Proof > category

changeset 868:35b2412a68e4

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 Wed, 08 Apr 2020 16:02:21 +0900
parents e47045bfc37a
children 65b7edb4db13
files CCCGraph1.agda
diffstat 1 files changed, 62 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Tue Apr 07 18:01:29 2020 +0900
+++ b/CCCGraph1.agda	Wed Apr 08 16:02:21 2020 +0900
@@ -83,17 +83,21 @@
    (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 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 )
+   (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)
 
-   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
+   _==_  : {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 π < 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)} = {!!}
@@ -101,6 +105,8 @@
    open import Data.Empty 
    open import Relation.Nullary 
 
+   open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
+
    isnot-∧ : (a : Objs) → Dec ( {x y : Objs } → ¬ a ≡ (x ∧ y ) )
    isnot-∧ (atom x) = yes ( λ {x} {y} () )
    isnot-∧ ⊤ = yes ( λ {x} {y} () )
@@ -108,7 +114,8 @@
    isnot-∧ (b <= a) = yes ( λ {x} {y} () )
 
    std-iv : {a b c d : Objs} (x : Arrow c d) (y : Arrow b c ) (f : Arrows a b) 
-        →  ( {x y : Objs } → ¬ b ≡ ( x ∧ y ) )   → eval (iv x ( iv y f ) ) ≡ iv x ( eval (iv y f ) )
+        →  ( {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)
@@ -122,16 +129,21 @@
    std-iv ε y (iv z f) ne | iv z1 t = refl
    std-iv (x *) y (iv z f) ne | iv z1 t = refl
 
-   std-∧ : { a b c : Objs } ( f : Arrows a b ) ( g : Arrows a b ) ( h : Arrows a c ) →  ¬ ( eval f ≡  iv π < g , h > ) 
-   std-∧ (iv f f1) g h t with eval ( iv f f1) | inspect eval (iv f f1 )
-   std-∧ (iv π < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f1 g h ee
-   std-∧ (iv π' < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f2 g h ee
-   std-∧ (iv x (iv f f1)) g h refl | iv π < g , h > | record { eq = ee } = {!!}  where
-      lemma : ¬ (  eval (iv x (iv f f1)) ≡ iv π < g , h > )
-      lemma ee = {!!}
-
-   std-∧' : { a b c : Objs } ( f : Arrows a c ) ( g : Arrows a b ) ( h : Arrows a c ) →  ¬ ( eval f ≡  iv π' < g , h > ) 
-   std-∧' = {!!}
+   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
@@ -139,29 +151,35 @@
    idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁)
    idem-eval (iv f (id a)) = refl
    idem-eval (iv f (○ a)) = refl
-   idem-eval (iv π < g , g₁ >) = idem-eval g 
+   idem-eval (iv π < g , g₁ >) = idem-eval g
    idem-eval (iv π' < g , g₁ >) = idem-eval g₁
    idem-eval (iv ε < f , f₁ >) = cong₂ ( λ j k → iv ε < j , k > ) (idem-eval f) (idem-eval f₁)
-   idem-eval (iv (x *) < f , f₁ >) =  cong₂ ( λ j k → iv (x *) < j , k > ) (idem-eval f) (idem-eval f₁)
-   idem-eval (iv f (iv {b} {c} {d} g h)) with eval (iv g h) | idem-eval (iv g h)  
-   idem-eval (iv f (iv {_} {_} {d} g h)) | id a | m = refl
-   idem-eval (iv f (iv {_} {_} {d} g h)) | ○ a | m = refl
-   idem-eval (iv π (iv {_} {_} {d} g h)) | < t , t₁ > | m = refl-<l> m
-   idem-eval (iv π' (iv {_} {_} {d} g h)) | < t , t₁ > | m = refl-<r> m
-   idem-eval (iv ε (iv {_} {_} {d} g h)) | < t , t₁ > | m = cong ( λ k → iv ε k ) m
-   idem-eval (iv (f *) (iv {_} {_} {d} g h)) | < t , t₁ > | m = cong ( λ k → iv (f *) k ) m
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {atom _} f1 t | m = trans (std-iv f f1 t (λ ()) ) (cong (λ k → iv f k ) m )
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {⊤} f1 t | m = trans (std-iv f f1 t (λ ()) ) (cong (λ k → iv f k ) m )
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {d1 <= d2} f1 t | m =  trans (std-iv f f1 t (λ ()) ) (cong (λ k → iv f k ) m )
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {d1 ∧ d2} f1 t | m = {!!}
-   --   lemma : eval (iv f (  iv f1 t)) ≡ iv f ( iv f1 t)
+   idem-eval (iv (x *) < f , f₁ >) = cong₂ ( λ j k → iv (x *) < j , k > ) (idem-eval f) (idem-eval f₁)
+   idem-eval (iv f (iv f₁ g)) = ?
+
+   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 = {!!}
+   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
+
+
+   ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
+   ==←≡ eq = cong (λ k → eval k ) eq
 
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
             _o_ =  λ{a} {b} {c} x y → x ・ y ;
-            _≈_ =  λ x y → x  ≡ y ;
+            _≈_ =  λ x y → x  == y ;
             Id  =  λ{a} → id a ;
             isCategory  = record {
                     isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
@@ -171,13 +189,13 @@
                     associative  = λ{a b c d f g h } → associative  f g h
                }
            }  where
-               identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
+               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₁} = {!!}
                associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
-                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
+                            (f ・ (g ・ h)) == ((f ・ g) ・ h)
                associative (id a) g h = {!!}
                associative (○ a) g h = refl
                associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
@@ -186,17 +204,23 @@
                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
-                       iv x (id _) ・ (g ・ h)
+                       eval (iv x (id _) ・ (g ・ h))
                     ≡⟨ {!!} ⟩
-                       (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
-                       iv x (iv y f) ・ (g ・ h)
+                       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)))
                     ≡⟨ {!!}  ⟩
-                       (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) 
                o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
-                            f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
+                            f == g → h == i → (h ・ f) == (i ・ g)
                o-resp-≈  f=g h=i = {!!}