Mercurial > hg > Members > kono > Proof > category

changeset 914:8c2da34e8dc1

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, 02 May 2020 05:32:42 +0900
parents c5446790ddb1
children fa302d99fa40 c10ee19a1ea3
files CCCGraph.agda deductive.agda
diffstat 2 files changed, 23 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sat May 02 04:25:05 2020 +0900
+++ b/CCCGraph.agda	Sat May 02 05:32:42 2020 +0900
@@ -414,11 +414,17 @@
        csc g = record { cat = CSC  ; ccc = cc1 ; ≡←≈ = λ eq → eq } where 
            open ccc-from-graph g
        cobj  : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c)  → Obj (cat (csc g)) → Obj (cat c)
-       cobj {g} {c} f (atom x) = {!!}
+       cobj {g} {c} f (atom x) = vmap f x
        cobj {g} {c} f ⊤ = CCC.１ (ccc c)
-       cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) {!!} {!!}
-       cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) {!!} {!!}
+       cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
+       cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
+       c-map : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} {A B : Obj (cat (csc g))}
+           → (f : Hom Grph g (FObj UX c) ) → Hom (cat (csc g)) A B → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
+       c-map {g} {c} {a} {atom x} f y = ?
+       c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
+       c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ w → proj₁ (z w))) (c-map f (λ w → proj₂ (z w)))
+       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) {!!}  -- with c-map f x
        solution : {g : Obj Grph} {c : Obj Cart} → Hom Grph g (FObj UX c) → Hom Cart (csc g) c
-       solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
+       solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = c-map {g} {c} f ; isFunctor = {!!} } ; ccf = {!!} }
 
 
--- a/deductive.agda	Sat May 02 04:25:05 2020 +0900
+++ b/deductive.agda	Sat May 02 05:32:42 2020 +0900
@@ -27,20 +27,23 @@
   -- every proof b →  c with assumption a has following forms
   
   data  φ  {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ) where
-     i : {b c : Obj A} {k : Hom A b c } → φ x k
-     ii : φ x {⊤} {a} x
+     i   : {b c : Obj A} {k : Hom A b c } → φ x k
+     ii  : φ x {⊤} {a} x
      iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
-     iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
-     v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
+     iv  : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
+     v   : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
   
   α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
   α = < π  ・ π   , < π'  ・ π  , π'  > >
   
   -- genetate (a ∧ b) → c proof from  proof b →  c with assumption a
   
-  kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x z ) → Hom A (a ∧ b) c
-  kx∈a x {k} i = k ・ π'
-  kx∈a x ii = π
-  kx∈a x (iii ψ χ ) = < kx∈a x ψ  , kx∈a x χ  >
-  kx∈a x (iv ψ χ ) = kx∈a x ψ  ・ < π , kx∈a x χ  >
-  kx∈a x (v ψ ) = ( kx∈a x ψ  ・ α ) *
+  k : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x∈a z ) → Hom A (a ∧ b) c
+  k x∈a {k} i = k ・ π'
+  k x∈a ii = π
+  k x∈a (iii ψ χ ) = < k x∈a ψ  , k x∈a χ  >
+  k x∈a (iv ψ χ ) = k x∈a ψ  ・ < π , k x∈a χ  >
+  k x∈a (v ψ ) = ( k x∈a ψ  ・ α ) *
+
+--  toφ : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
+--  toφ {a} {b} {c} x∈a z = {!!}