Mercurial > hg > Members > kono > Proof > category

changeset 811:2de0358ea10a

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 Sat, 27 Apr 2019 07:09:35 +0900
parents 084dc5e170f8
children 4ff300e1e98c
files CCChom.agda discrete.agda
diffstat 2 files changed, 73 insertions(+), 71 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Fri Apr 26 22:53:57 2019 +0900
+++ b/CCChom.agda	Sat Apr 27 07:09:35 2019 +0900
@@ -618,8 +618,10 @@
    open SM
 
    -- positive intutionistic calculus
+   PL : (G : SM) → Graph
+   PL G = record { vertex = Objs {graph G} ; edge = Arrow {graph G}} 
    DX : (G : SM) → Category  Level.zero Level.zero Level.zero   
-   DX G = GraphtoCat ( record { vertex = Objs {graph G} ; edge = Arrow {graph G}} )
+   DX G = GraphtoCat (PL G)
 
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
@@ -631,86 +633,85 @@
    fobj ⊤ = One'
    fmap : {G : SM} { a b : Obj (DX G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
    fmap {G} {a} {a} (id a) = λ z → z
-   fmap {G} {a} {(atom b)} (next {a} {c} (arrow x) f) = λ z → smap G x ( k z ) where
-       k : fobj a → fobj {G} c 
-       k z = fmap f z
+   fmap {G} {a} {(atom b)} (next {a} {c} (arrow x) f) = λ (z : fobj a) → smap G x ( fmap f z ) 
    fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
-   fmap {G} {a} {b} (next {a} {b ∧ y} {b} π f) = λ z → proj₁ ( k z ) where
-       k : fobj a → fobj b /\ fobj y  
-       k z = fmap f z
-   fmap {G} {a} {b} (next {.a} {x ∧ b} π' f) =  λ z → proj₂ ( k z ) where
-       k : fobj a → fobj x /\ fobj b  
-       k z = fmap f z
-   fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) =  λ z → (  proj₁ (k z))(  proj₂ (k z)) where
-       k :  fobj a →  (fobj y → fobj x) /\ fobj y
-       k z = fmap f z
+   fmap {G} {a} {b} (next {a} {.b ∧ y} {b} π f) = λ z → proj₁ ( fmap {G} {a} {b ∧ y} f z ) 
+   fmap {G} {a} {b} (next {.a} {x ∧ .b} {.b} π' f) =  λ z → proj₂ ( fmap f z ) where
+   fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) =  λ z → (  proj₁ (fmap f z))(  proj₂ (fmap f z)) 
 
    CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
    FObj (CS G) a  = fobj a
    FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
    isFunctor (CS G) = isf where
        _++_ = Category._o_ (DX G)
-       distrCS : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → Sets [ fmap ((DX G) [ g o f ]) ≈ Sets [ fmap g o fmap f ] ]
-       distrCS {a} {.a} {.a} {id a} {id .a} = refl
-       distrCS {a} {.a} {c} {id a} {next x g} = begin
-             fmap (DX G [ next x g o Chain.id a ])
-          ≈⟨⟩
-             fmap ( next x ( g ++ (Chain.id a)))
-          ≈⟨ extensionality Sets ( λ y → cong ( λ k → fmap ( next x k ) y ) (idR1 (DX G)) ) ⟩
-             fmap ( next x  g )
-          ≈↑⟨ refl ⟩
-             Sets [ fmap (next x g) o fmap (Chain.id a) ]
-          ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {b} {f} {id b} =  refl
-       distrCS {a} {b} {atom z} {f} {next {.b} {atom y} {atom z} (arrow x) g} = begin
-             fmap (DX G [ next (arrow x) g o f ])
-          ≈⟨⟩
-             fmap ( next (arrow x) (g ++ f ) )
-          ≈⟨⟩
-             ( λ y → smap G x ( fmap (g ++ f) y )  )
-          ≈⟨ extensionality Sets ( λ y → ( cong ( λ k → smap G x (k y) ) distrCS )) ⟩
-             (λ z → fmap (next (arrow x) g) ( fmap f z ))
-          ≈⟨⟩
-             (Sets [ fmap (next (arrow x) g) o fmap f ])
-          ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
-             fmap (DX G [ next (○ a₁) g o f ])
-          ≈⟨⟩
-             Sets [ fmap (next (○ a₁) g) o fmap f ]
-          ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} =  begin
-             fmap (DX G [ next π g o f ])
-          ≈⟨⟩
-             fmap (next π (g ++ f))
-          ≈⟨  extensionality Sets ( λ z → (cong ( λ k → k z) refl ))  ⟩
-             ( λ z → proj₁ (fmap (g ++ f) z))
-          ≈⟨ extensionality Sets ( λ z → cong ( λ k → proj₁ (k z)  ) distrCS )  ⟩
-             Sets [ fmap (next π g) o fmap f ]
-          ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {c} {f} {next π' g} =   begin
-             fmap (DX G [ next π' g o f ])
-          ≈⟨⟩
-             fmap (next π' (g ++ f))
-          ≈⟨  extensionality Sets ( λ z → (cong ( λ k → k z) refl ))  ⟩
-             ( λ z → proj₂ (fmap (g ++ f) z))
-          ≈⟨ extensionality Sets ( λ z → cong ( λ k → proj₂ (k z)  ) distrCS )  ⟩
-             Sets [ fmap (next π' g) o fmap f ]
-          ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {c} {f} {next ε g} =  begin
-             fmap (DX G [ next ε g o f ] )
-          ≈⟨⟩
-              fmap (next ε (g ++ f))
-          ≈⟨  extensionality Sets ( λ z → (cong ( λ k → k z) refl )) ⟩
-             ( λ z →  proj₁ (fmap (g ++ f)  z) (  proj₂ (fmap (g ++ f) z) ))
-          ≈⟨  extensionality Sets ( λ z → cong ( λ k → proj₁ (k z) (  proj₂ (k z))  ) distrCS )    ⟩
-             ( λ x → fmap (next ε g) (fmap f x) )
-          ≈⟨⟩
-             Sets [ fmap (next ε g) o fmap f ]
-          ∎  where open ≈-Reasoning Sets
+       ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
+       distr : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
+       distr {a} {.a} {.a} {id a} {id .a} z =  refl
+       distr {a} {.a} {c} {id a} {next x g} z = begin
+             fmap (DX G [ next x g o Chain.id a ]) z
+          ≡⟨⟩
+             fmap ( next x ( g ++ (Chain.id a))) z
+          ≡⟨ cong ( λ k → fmap ( next x k ) z ) ++idR  ⟩
+             fmap ( next x  g ) z
+          ≡⟨ refl ⟩
+             ( Sets [ fmap (next x g) o fmap (Chain.id a) ] ) z
+          ∎  where open ≡-Reasoning 
+       distr {a} {b} {b} {f} {id b} z =  refl
+       distr {a} {b} {atom z} {f} {next {.b} {atom y} {atom z} (arrow x) g} w =  begin
+             fmap (DX G [ next (arrow x) g o f ]) w
+          ≡⟨⟩
+             fmap ( next (arrow x) (g ++ f ) ) w
+          ≡⟨⟩
+             smap G x ( fmap (g ++ f) w )   
+          ≡⟨ cong ( λ k → smap G x k ) (distr {a} {b} {atom y} {f} {g} w) ⟩
+             smap G x (fmap g (fmap f w))
+          ≡⟨⟩
+             fmap (next (arrow x) g) ( fmap f w )
+          ≡⟨⟩
+             (Sets [ fmap (next (arrow x) g) o fmap f ]) w
+          ∎  where open ≡-Reasoning 
+       distr {a} {b} {.⊤} {f} {next (○ a₁) g} z = begin
+             fmap (DX G [ next (○ a₁) g o f ]) z
+          ≡⟨⟩
+             (Sets [ fmap (next (○ a₁) g) o fmap f ]) z
+          ∎  where open ≡-Reasoning 
+       distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z =  begin
+             fmap (DX G [ next π g o f ]) z
+          ≡⟨⟩
+             fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z
+          ≡⟨ {!!} ⟩
+             proj₁ ( fmap {G} {a} {c ∧ x} (g ++ f ) z ) 
+          ≡⟨ cong ( λ k → proj₁ k ) ( distr {a} {b} {(c ∧ x)} {f} {g} z )  ⟩
+             proj₁ ( fmap g ( fmap f z ))
+          ≡⟨ {!!} ⟩
+             (Sets [ fmap (next π g) o fmap f ]) z
+          ∎  where open ≡-Reasoning 
+       distr {a} {b} {c} {f} {next π' g} z =   begin
+             fmap (DX G [ next π' g o f ]) z
+          ≡⟨⟩
+             fmap (next π' (g ++ f)) z
+          ≡⟨ {!!} ⟩
+             proj₂ (fmap (g ++ f) z)
+          ≡⟨ {!!} ⟩
+             ( Sets [ fmap (next π' g) o fmap f ] ) z
+          ∎  where open ≡-Reasoning 
+       distr {a} {b} {c} {f} {next {b} {(c <= x) ∧ x} {c} ε g} z =  begin
+             fmap (DX G [ next ε g o f ] ) z
+          ≡⟨⟩
+              fmap (next ε (g ++ f)) z
+          ≡⟨ {!!} ⟩
+             proj₁ (fmap (g ++ f)  z) (  proj₂ (fmap (g ++ f) z) ) 
+          ≡⟨  cong ( λ k → proj₁ k (  proj₂ k)) (distr {a} {b} {(c <= x) ∧ x} {f} {g} z)   ⟩
+             proj₁ (fmap g (fmap f z)) ( proj₂ (fmap g (fmap f z)))
+          ≡⟨ {!!} ⟩
+             fmap (next ε g) (fmap f z) 
+          ≡⟨⟩
+             ( Sets [ fmap (next ε g) o fmap f ] ) z
+          ∎  where open ≡-Reasoning 
        isf : IsFunctor (DX G) Sets fobj fmap 
        IsFunctor.identity isf = extensionality Sets ( λ x → refl )
        IsFunctor.≈-cong isf refl = refl
-       IsFunctor.distr isf {a} {b} {c} {g} {f} = distrCS {a} {b} {c} {g} {f}
+       IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
    <_,_> : { G : SM } → {a b c : Objs {graph G}} → Arrow c a → Arrow c b → Hom Sets (FObj (CS G) c ) (FObj (CS G) (a ∧ b) )
    <_,_> {G} {a} {b} {c}   f  g  = λ z → ( (FMap (CS G) ( next f (id c)))  z , FMap (CS G) (next g (id c)) z )
--- a/discrete.agda	Fri Apr 26 22:53:57 2019 +0900
+++ b/discrete.agda	Sat Apr 27 07:09:35 2019 +0900
@@ -22,6 +22,7 @@
   _・_ : { G : Graph} {a b c : Graph.vertex G } (f : Chain {G} b c ) → (g : Chain {G} a b) → Chain {G} a c
   id _ ・ f = f
   (next x f) ・ g = next x ( f ・ g )
+  -- _・_ {G} {a} {b} {c} (next {b} {d} {c} x f)  g = next {G} {a} {d} {c} x ( f ・ g )
 
   GraphtoCat : (G : Graph )  →  Category  Level.zero Level.zero Level.zero   
   GraphtoCat G = record {