# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1555904629 -32400
# Node ID ba575c73ea48d9525ba270754e3577bc6c858e3e
# Parent  f37f11e1b8716a9a8151edac393362e7bc36d924
...

diff -r f37f11e1b871 -r ba575c73ea48 CCC.agda
--- a/CCC.agda	Mon Apr 22 02:41:53 2019 +0900
+++ b/CCC.agda	Mon Apr 22 12:43:49 2019 +0900
@@ -52,8 +52,8 @@
         ≈⟨ e3c ⟩
           id1 A (a ∧ b )
         ∎
-     distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
-     distr {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
+     distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
+     distr-π {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
             < f , g > o h
         ≈↑⟨ e3c ⟩
             < π o  < f , g > o h  , π' o  < f , g > o h  >
@@ -62,8 +62,51 @@
         ≈⟨ π-cong (car e3a ) (car e3b) ⟩
             < f o h ,  g o h  >
         ∎
-     _×_ :  {  a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e )
-     f × g  = λ h →  < A [ f o A [ π o h  ] ] , A [ g o A [ π' o h ] ] >
+     _×_ :  {  a b c d  : Obj A } ( f : Hom A a c ) (g : Hom A b d )  → Hom A (a ∧ b) ( c ∧ d )
+     f × g  = < (A [ f o  π ] ) , (A [ g o π' ])  >
+     distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → A [ A [ h * o k ]  ≈ ( A [ h o < A [ k o π ] , π' > ] ) * ]
+     distr-* {a} {b} {c} {d} {h} {k} = begin
+             h * o k
+        ≈↑⟨ e4b  ⟩
+             (  ε o < (h * o k ) o π  , π' > ) *
+        ≈⟨ *-cong ( begin
+              ε o < (h * o k ) o π  , π' > 
+        ≈↑⟨ cdr ( π-cong assoc refl-hom ) ⟩
+              ε o ( < h * o ( k o π ) , π' > ) 
+        ≈↑⟨ cdr ( π-cong (cdr e3a) e3b ) ⟩
+               ε o ( < h * o ( π o < k o π , π' > ) , π' o < k o π , π' > > ) 
+        ≈⟨ cdr ( π-cong assoc refl-hom) ⟩
+               ε o ( < (h * o π) o < k o π , π' > , π' o < k o π , π' > > ) 
+        ≈↑⟨ cdr ( distr-π ) ⟩
+               ε o ( < h * o π , π' >  o < k o π , π' > )
+        ≈⟨ assoc ⟩
+              ( ε o < h * o π , π' > ) o < k o π , π' > 
+        ≈⟨ car e4a  ⟩
+               h o < k o π , π' > 
+        ∎ ) ⟩
+            ( h o  <  k o π  , π' > ) *
+        ∎ where open  ≈-Reasoning A
+     α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
+     α = < A [ π  o π  ]  , < A [ π'  o π ]  , π'  > >
+     α' : {a b c : Obj A } → Hom A  ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c )
+     α' = < < π , A [ π o π' ] > ,  A [ π'  o π' ]  >
+     β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → A [ A [ α o < < f , g > , h > ] ≈  < f , < g , h > > ]
+     β {a} {b} {c} {d} {f} {g} {h} = begin
+             α o < < f , g > , h >
+        ≈⟨⟩
+            ( < ( π o π ) , < ( π' o π ) , π' > > ) o  < < f , g > , h >
+        ≈⟨ distr-π ⟩
+             < ( ( π o π ) o  < < f , g > , h > ) , ( < ( π' o π ) , π' >   o  < < f , g > , h > )  >  
+        ≈⟨ π-cong refl-hom distr-π ⟩
+             < ( ( π o π ) o  < < f , g > , h > ) , ( < ( ( π' o π ) o  < < f , g > , h > ) , ( π'  o  < < f , g > , h > ) > )  >  
+        ≈↑⟨ π-cong assoc ( π-cong assoc refl-hom )  ⟩
+             < (  π o (π  o  < < f , g > , h >) ) , ( < (  π' o ( π  o  < < f , g > , h > ) ) , ( π'  o  < < f , g > , h > ) > )  >  
+        ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b )  ⟩
+             < (  π o < f , g >  ) ,  < (  π' o < f , g >  ) , h >   >  
+        ≈⟨ π-cong e3a ( π-cong e3b refl-hom )  ⟩
+            < f , < g , h > >
+         ∎ where open  ≈-Reasoning A
+
 
 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
      field
diff -r f37f11e1b871 -r ba575c73ea48 CCChom.agda
--- a/CCChom.agda	Mon Apr 22 02:41:53 2019 +0900
+++ b/CCChom.agda	Mon Apr 22 12:43:49 2019 +0900
@@ -85,7 +85,7 @@
           ; ccc-3 =   record {   ≅→ =  c301 ; ≅← = c302 ; iso→  = c303 ; iso←  = c304 ; cong← = c305 ; cong→ = c306 }
           ; nat-2 = nat-2 ; nat-3 = nat-3
         }
-   } where
+   } module CCC→HOM where
       c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj
       c101 _  = OneObj
       c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c)
@@ -166,11 +166,54 @@
                  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
+U_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A)  → Functor A A
+FObj (U_b A ccc b) = λ a → (CCC._<=_ ccc  a b )
+FMap (U_b A ccc b) = λ f → CCC._* ccc ( A [ f o  CCC.ε ccc ] ) 
+isFunctor (U_b A ccc b) = isF where
+   isF : IsFunctor A A ( λ a → (CCC._<=_ ccc  a b)) (  λ f → CCC._* ccc ( A [ f o  CCC.ε ccc ] ) )
+   IsFunctor.≈-cong isF f≈g = IsCCC.*-cong (CCC.isCCC ccc) ( car f≈g ) where open ≈-Reasoning A
+   --    e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]
+   IsFunctor.identity isF {a} = begin
+                 (ccc CCC.*) (A [ id1 A a o CCC.ε ccc ])
+             ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( begin
+                  id1 A a o CCC.ε ccc
+             ≈⟨  idL  ⟩
+                  CCC.ε ccc
+             ≈↑⟨  idR  ⟩
+                  CCC.ε ccc o id1 A (CCC._∧_ ccc ( CCC._<=_ ccc a b ) b )
+             ≈↑⟨  cdr ( IsCCC.π-id (CCC.isCCC ccc)) ⟩
+                   CCC.ε ccc o ( CCC.<_,_> ccc ( CCC.π ccc ) (CCC.π' ccc) )
+             ≈↑⟨  cdr ( IsCCC.π-cong (CCC.isCCC ccc) idL refl-hom)  ⟩
+                   CCC.ε ccc o ( CCC.<_,_> ccc ( id1 A (CCC._<=_ ccc a b)  o CCC.π ccc ) (CCC.π' ccc) )
+                  ∎ ) ⟩
+                 (ccc CCC.*) (  CCC.ε ccc o ( CCC.<_,_> ccc ( id1 A (CCC._<=_ ccc a b)  o CCC.π ccc ) (CCC.π' ccc) ))
+             ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩
+                 id1 A ((ccc CCC.<= a) b)
+             ∎ where open ≈-Reasoning A
+   IsFunctor.distr isF {x} {y} {z} {f} {g} = begin
+                (ccc CCC.*) ( ( g o f ) o CCC.ε ccc )
+             ≈⟨ {!!} ⟩
+                (ccc CCC.*) (( g o CCC.ε ccc ) o  CCC.<_,_> ccc ((ccc CCC.*)
+                    (  f o ( CCC.ε ccc  o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc)))) (CCC.π' ccc))
+             ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( cdr ( IsCCC.π-cong (CCC.isCCC ccc) ( begin
+                (ccc CCC.*) (  f o ( CCC.ε ccc  o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc)))
+             ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) assoc  ⟩
+                 (ccc CCC.*) (( f o CCC.ε ccc ) o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc))
+             ≈↑⟨ IsCCC.distr-* (CCC.isCCC ccc) ⟩
+                 (ccc CCC.*) ( f o CCC.ε ccc )  o CCC.π ccc 
+             ∎ )  refl-hom )) ⟩
+                 (ccc CCC.*) (( g o CCC.ε ccc ) o  CCC.<_,_> ccc ( (ccc CCC.*) ( f o CCC.ε ccc )  o CCC.π ccc )  (CCC.π' ccc)  ) 
+             ≈↑⟨ IsCCC.distr-* (CCC.isCCC ccc) ⟩
+                 (ccc CCC.*) ( g o CCC.ε ccc )  o (ccc CCC.*) ( f o CCC.ε ccc )  
+             ∎ where open ≈-Reasoning A
+
+
+
+c^b=b<=c : {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  ] )
+c^b=b<=c A ccc {a} {b} {c} = record {
+           ≅→ = λ f → A [ CCC.ε ccc o  CCC.<_,_> ccc ( A [ f o CCC.○ ccc b ] ) ( id1 A b )  ] ---   g ’   (g : 1 → b ^ a) of
+       ;   ≅← =  λ f → CCC._* ccc ( A [ f o  CCC.π' ccc  ] )                                  --- ┌ f ┐   name of (f : b ^a → 1 )
        ;   iso→  = iso→
        ;   iso←  = iso←
        ;   cong→ = cong*
@@ -188,7 +231,7 @@
                  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 ) ) ⟩
+             ≈↑⟨ 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)
@@ -222,7 +265,7 @@
                 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 ) ) ) ⟩
+             ≈⟨ 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) )