# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562944697 -32400
# Node ID 6c5cfb9b333e874b99d010058f40ad6719d70093
# Parent  8127654aee5eb88ccbfa324a4fca56ad1567388b
fix deduction theorem

diff -r 8127654aee5e -r 6c5cfb9b333e CCCGraph.agda
--- a/CCCGraph.agda	Thu May 09 08:34:52 2019 +0900
+++ b/CCCGraph.agda	Sat Jul 13 00:18:17 2019 +0900
@@ -268,7 +268,7 @@
 _&_ :  {v v' : Level} {x y z : Graph {v} {v'}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
 f & g = record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
 
-Grph : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (suc ( v ⊔ v'))
+Grph : {v v' : Level} → Category (suc (v ⊔ v')) (suc (v ⊔ v')) (suc ( v ⊔ v'))
 Grph {v} {v'} = record {
     Obj = Graph {v} {v'}
   ; Hom = GMap {v} {v'}
diff -r 8127654aee5e -r 6c5cfb9b333e deductive.agda
--- a/deductive.agda	Thu May 09 08:34:52 2019 +0900
+++ b/deductive.agda	Sat Jul 13 00:18:17 2019 +0900
@@ -27,20 +27,20 @@
   -- 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 ψ  ・ α ) *