# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1555868513 -32400
# Node ID f37f11e1b8716a9a8151edac393362e7bc36d924
# Parent  5bee48f7c126c6f027d662a792b3f8f826673261
Hom a,b = Hom 1 b^a

diff -r 5bee48f7c126 -r f37f11e1b871 CCC.agda
--- a/CCC.agda	Sun Apr 21 18:11:14 2019 +0900
+++ b/CCC.agda	Mon Apr 22 02:41:53 2019 +0900
@@ -22,7 +22,7 @@
              :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
        -- cartesian
-       e2  : {a : Obj A} → ∀ ( f : Hom A a １ ) →  A [ f ≈ ○ a ]
+       e2  : {a : Obj A} → ∀ { f : Hom A a １ } →  A [ f ≈ ○ a ]
        e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o < f , g > ] ≈ f ]
        e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π' o < f , g > ] ≈ g ]
        e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } →  A [ < A [ π o h ] , A [ π' o h  ] >  ≈ h ]
@@ -35,13 +35,13 @@
      e'2 : A [ ○ １ ≈ id1 A １ ]
      e'2 = let open  ≈-Reasoning A in begin
             ○ １
-        ≈↑⟨ e2 (id1 A １ ) ⟩
+        ≈↑⟨ e2  ⟩
            id1 A １
         ∎
      e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [  ○ b o f ] ≈ ○ a ]
      e''2 {a} {b} {f} = let open  ≈-Reasoning A in begin
            ○ b o f
-        ≈⟨ e2 (○ b o f) ⟩
+        ≈⟨ e2  ⟩
            ○ a
         ∎
      π-id : {a b : Obj A} → A [ < π ,  π' >  ≈ id1 A (a ∧ b ) ]
diff -r 5bee48f7c126 -r f37f11e1b871 CCChom.agda
--- a/CCChom.agda	Sun Apr 21 18:11:14 2019 +0900
+++ b/CCChom.agda	Mon Apr 22 02:41:53 2019 +0900
@@ -93,7 +93,7 @@
       c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f 
       c103 {a} {OneObj} {OneObj} {OneObj} = refl
       c104 : {a : Obj A} →  {f : Hom A a (CCC.１ c)} → A [ (c102 ( c101 f )) ≈ f ]
-      c104 {a} {f} = let  open  ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f ) 
+      c104 {a} {f} = let  open  ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c)  ) 
       c201 :  { c₁ a b  : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b)
       c201 f = ( A [ CCC.π c o f ]  , A  [ CCC.π' c o f ] )
       c202 :  { c₁ a b  : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b)
@@ -166,6 +166,86 @@
                  c301 k
              ∎ where open ≈-Reasoning A
 
+lemma1 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} →  -- Hom A １ ( c ^ b ) ≅ Hom A b c
+                          IsoS A A  (CCC.１ ccc ) (CCC._<=_ ccc  c b) b c
+lemma1 A ccc {a} {b} {c} = record {
+           ≅→ = λ f → A [ CCC.ε ccc o  CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b )  ]
+       ;   ≅← =  λ f → CCC._* ccc ( A [ f o  CCC.π' ccc  ] )
+       ;   iso→  = iso→
+       ;   iso←  = iso←
+       ;   cong→ = cong*
+       ;   cong← = cong2
+   } where
+       cc = IsCCChom.ccc-3 ( CCChom.isCCChom (CCC→hom  A ccc ) ) 
+       -- e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } →  A [ A [ ε o ( <,> ( A [ (k *) o π ] )   π')  ] ≈ k ]
+       iso→ : {f : Hom A b c} → A [
+            (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o (ccc CCC.*) ((A Category.o f) (CCC.π' ccc))) (CCC.○ ccc b) > (Category.Category.Id A)) ≈ f ]
+       iso→ {f} = begin
+               CCC.ε ccc o (CCC.<_,_> ccc  (CCC._* ccc ( f o (CCC.π' ccc)) o (CCC.○ ccc b)) (id1 A b )  )
+             ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) refl-hom (IsCCC.e3b (CCC.isCCC ccc) ) ) ⟩
+                 CCC.ε ccc   o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.○ ccc b) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) )  )
+             ≈↑⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) (cdr (IsCCC.e3a (CCC.isCCC ccc))) refl-hom )  ⟩
+                 CCC.ε ccc   o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o ( CCC.π ccc  o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) )  )
+             ≈⟨ cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) assoc refl-hom ) ⟩
+                 CCC.ε ccc   o ( CCC.<_,_> ccc ((CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b)  ) ((CCC.π' ccc) o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) )  )
+             ≈↑⟨ cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ⟩
+                 CCC.ε ccc   o ( CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc)   o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) )
+             ≈⟨ assoc ⟩
+                ( CCC.ε ccc   o  CCC.<_,_> ccc (CCC._* ccc (f o CCC.π' ccc) o CCC.π ccc ) (CCC.π' ccc) )  o CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b)
+             ≈⟨ car ( IsCCC.e4a (CCC.isCCC ccc) )  ⟩
+               ( f o  CCC.π' ccc ) o  CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) 
+             ≈↑⟨ assoc ⟩
+               f o ( CCC.π' ccc  o  CCC.<_,_> ccc (CCC.○ ccc b) (id1 A b) ) 
+             ≈⟨ cdr (IsCCC.e3b (CCC.isCCC ccc)) ⟩
+               f o id1 A b 
+             ≈⟨ idR ⟩
+               f
+             ∎ where open ≈-Reasoning A
+       lemma : {f : Hom A (CCC.１ ccc) ((ccc CCC.<= c) b)} → A [ A [ A [ f o (CCC.○ ccc b) ] o  (CCC.π' ccc) ]  ≈ A [  f o (CCC.π ccc) ] ]
+       lemma {f} = begin
+                   ( f o (CCC.○ ccc b) ) o  (CCC.π' ccc)
+               ≈↑⟨ assoc  ⟩
+                   f o ( (CCC.○ ccc b) o  (CCC.π' ccc) )
+               ≈⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) )  ⟩
+                   f o (CCC.○ ccc ( CCC._∧_ ccc (CCC.１ ccc) b ) )
+               ≈↑⟨ cdr ( IsCCC.e2 (CCC.isCCC ccc) )  ⟩
+                   f o ( (CCC.○ ccc) (CCC.１ ccc) o (CCC.π ccc) )
+               ≈↑⟨ cdr ( car ( IsCCC.e2 (CCC.isCCC ccc) ))  ⟩
+                   f o ( id1 A (CCC.１ ccc) o (CCC.π ccc) )
+               ≈⟨ cdr (idL) ⟩
+                   f o (CCC.π ccc)
+               ∎ where open ≈-Reasoning A
+       --     e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o ( <,> ( A [ k o  π ]  )  π' ) ] ) * ≈ k ]
+       iso← : {f : Hom A (CCC.１ ccc) ((ccc CCC.<= c) b)} → A [  (ccc CCC.*) ((A Category.o (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) >
+                          (Category.Category.Id A))) (CCC.π' ccc)) ≈ f ]
+       iso← {f} = begin
+                CCC._* ccc (( CCC.ε ccc o ( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b ))) o (CCC.π' ccc))
+             ≈↑⟨ IsCCC.*-cong ( CCC.isCCC ccc ) assoc ⟩
+                CCC._* ccc ( CCC.ε ccc o (( CCC.<_,_> ccc ( f o (CCC.○ ccc b) ) (id1 A b )) o (CCC.π' ccc)))
+             ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.distr ( CCC.isCCC ccc ) ) ) ⟩
+                CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( (f o (CCC.○ ccc b)) o  CCC.π' ccc ) (id1 A b o CCC.π' ccc) )
+             ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (cdr ( IsCCC.π-cong ( CCC.isCCC ccc ) lemma idL )) ⟩
+                CCC._* ccc ( CCC.ε ccc o CCC.<_,_> ccc ( f o CCC.π ccc ) (CCC.π' ccc) )
+             ≈⟨  IsCCC.e4b (CCC.isCCC ccc)  ⟩
+               f
+             ∎ where open ≈-Reasoning A
+       cong* :  {f g : Hom A (CCC.１ ccc) ((ccc CCC.<= c) b)} →
+            A [ f ≈ g ] → A [ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o f) (CCC.○ ccc b) > (Category.Category.Id A))
+            ≈ (A Category.o CCC.ε ccc) (CCC.< ccc , (A Category.o g) (CCC.○ ccc b) > (Category.Category.Id A)) ]
+       cong* {f} {g} f≈g = begin
+                CCC.ε ccc o (  CCC.<_,_> ccc ( f o ( CCC.○ ccc b )) (id1 A b ))
+             ≈⟨ cdr (IsCCC.π-cong ( CCC.isCCC ccc ) (car f≈g) refl-hom  )  ⟩
+                CCC.ε ccc o (  CCC.<_,_> ccc ( g o ( CCC.○ ccc b )) (id1 A b ))
+             ∎ where open ≈-Reasoning A
+       cong2 : {f g : Hom A b c} → A [ f ≈ g ] →
+            A [ (ccc CCC.*) ((A Category.o f) (CCC.π' ccc)) ≈ (ccc CCC.*) ((A Category.o g) (CCC.π' ccc)) ]
+       cong2 {f} {g} f≈g = begin
+                CCC._* ccc ( f o (CCC.π' ccc) )
+             ≈⟨ IsCCC.*-cong ( CCC.isCCC ccc ) (car f≈g ) ⟩
+                CCC._* ccc ( g o (CCC.π' ccc) )
+             ∎ where open ≈-Reasoning A
+
+
 
 
 open CCChom
@@ -216,8 +296,8 @@
            } where
                e20 : ∀ ( f : Hom OneCat OneObj OneObj ) →  _[_≈_] OneCat {OneObj} {OneObj} f OneObj 
                e20 OneObj = refl
-               e2  : {a : Obj A} → ∀ ( f : Hom A a １ ) →  A [ f ≈ ○ a ]
-               e2 {a} f = begin
+               e2  : {a : Obj A} → ∀ { f : Hom A a １ } →  A [ f ≈ ○ a ]
+               e2 {a} {f} = begin
                      f
                   ≈↑⟨  iso← ( ccc-1 (isCCChom h )) ⟩
                     ≅← ( ccc-1 (isCCChom h )  {a} {OneObj} {OneObj}) (  ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f ) 
@@ -363,8 +443,8 @@
              ; e4b = e4b
              ; *-cong = *-cong
            } where
-                e2 : {a : Obj Sets} (f : Hom Sets a １) → Sets [ f ≈ ○ a ]
-                e2 {a} f = extensionality Sets ( λ x → e20 x )
+                e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ]
+                e2 {a} {f} = extensionality Sets ( λ x → e20 x )
                   where
                         e20 : (x : a ) → f x ≡ ○ a x
                         e20 x with f x
diff -r 5bee48f7c126 -r f37f11e1b871 deductive.agda
--- a/deductive.agda	Sun Apr 21 18:11:14 2019 +0900
+++ b/deductive.agda	Mon Apr 22 02:41:53 2019 +0900
@@ -36,9 +36,9 @@
 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
-   iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x < f , g > 
+   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 ( f * )
+   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 ) )
 α = < π  ・ π   , < π'  ・ π  , π'  > >