changeset 795:030c5b87ed78

ccc to adjunction done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Apr 2019 18:00:03 +0900
parents ba575c73ea48
children 472a615c6e09
files CCChom.agda
diffstat 1 files changed, 122 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Mon Apr 22 12:43:49 2019 +0900
+++ b/CCChom.agda	Mon Apr 22 18:00:03 2019 +0900
@@ -4,7 +4,7 @@
 
 open import HomReasoning
 open import cat-utility
-open import Data.Product renaming (_×_ to _∧_)
+open import Data.Product renaming (_×_ to _/\_  ) hiding ( <_,_> )
 open import Category.Constructions.Product
 open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
@@ -170,43 +170,115 @@
 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 ] ) )
+   _<=_ = CCC._<=_ ccc
+   _∧_ = CCC._∧_ ccc
+   <_,_> = CCC.<_,_> ccc
+   _* = CCC._* ccc
+   ε = CCC.ε ccc
+   π = CCC.π ccc
+   π' = CCC.π' ccc
+   isc = CCC.isCCC ccc
+   *-cong = IsCCC.*-cong (CCC.isCCC ccc)
+   π-cong = IsCCC.π-cong (CCC.isCCC ccc)
+
+   isF : IsFunctor A A ( λ a → (a <=  b)) (  λ f → CCC._* ccc ( A [ f o  ε ] ) )
    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 ])
+                 (id1 A a o ε ) * 
              ≈⟨ 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) ))
+                  ε o id1 A ( ( a <= b ) ∧ b )
+             ≈↑⟨  cdr ( IsCCC.π-id isc) ⟩
+                   ε o ( < π , π'  > )
+             ≈↑⟨  cdr ( π-cong  idL refl-hom)  ⟩
+                   ε o ( < id1 A (a <= b)  o π , π' > )
+             ∎ ) ⟩
+                  (  ε o ( < id1 A ( a <= b)  o π ,  π'  > ) ) *
              ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩
-                 id1 A ((ccc CCC.<= a) b)
+                 id1 A (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 )  
+                 ( ( g o f ) o ε ) *
+             ≈↑⟨ *-cong assoc ⟩
+                 (  g o (f o ε ) ) *
+             ≈↑⟨ *-cong ( cdr (IsCCC.e4a isc) ) ⟩
+                  ( g o ( ε  o ( < ( ( f o ε ) * ) o π , π' > ) )) *
+             ≈⟨ *-cong assoc ⟩
+                  ( ( g o ε ) o ( < ( ( f o ε ) * ) o π , π' > ) ) *
+             ≈↑⟨ IsCCC.distr-* isc ⟩
+                  ( g o ε ) *  o  ( f o ε ) *  
+             ∎ where open ≈-Reasoning A
+
+F_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A)  → Functor A A
+FObj (F_b A ccc b) = λ a → ( CCC._∧_ ccc a  b )
+FMap (F_b A ccc b) = λ f → ( CCC.<_,_>  ccc (A [ f o CCC.π ccc ] ) ( CCC.π'  ccc) )
+isFunctor (F_b A ccc b) = isF where
+   _∧_ = CCC._∧_ ccc
+   <_,_> = CCC.<_,_> ccc
+   π = CCC.π ccc
+   π' = CCC.π' ccc
+   isc = CCC.isCCC ccc
+   π-cong = IsCCC.π-cong (CCC.isCCC ccc)
+
+   isF : IsFunctor A A ( λ a → (a ∧  b)) (  λ f → < ( A [ f o π ] ) , π' >  )
+   IsFunctor.≈-cong isF f≈g = π-cong ( car f≈g ) refl-hom  where open ≈-Reasoning A
+   IsFunctor.identity isF {a} = trans-hom (π-cong idL refl-hom ) (IsCCC.π-id isc)  where open ≈-Reasoning A
+   IsFunctor.distr isF {x} {y} {z} {f} {g} = begin
+                 < ( g o f ) o π  , π' >
+             ≈↑⟨ π-cong assoc refl-hom ⟩
+                 <  g o ( f o π ) , π' >
+             ≈↑⟨  π-cong (cdr (IsCCC.e3a isc )) refl-hom ⟩
+                 <  g o ( π  o < ( f o π ) , π' > ) , π' >
+             ≈⟨  π-cong  assoc ( sym-hom (IsCCC.e3b isc ))  ⟩
+                 < ( g o π )  o < ( f o π ) , π' > , π'  o < ( f o π ) , π' > >
+             ≈↑⟨ IsCCC.distr-π isc ⟩
+                 < ( g o π ) , π' > o < ( f o π ) , π' > 
              ∎ where open ≈-Reasoning A
 
+CCCtoAdj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (  ccc : CCC A ) → (b : Obj A ) → coUniversalMapping A A (F_b A ccc b)
+CCCtoAdj  A ccc b = record {
+        U  = λ a → a <= b 
+   ;    ε  = ε'
+   ;    _*'  = solution
+   ;    iscoUniversalMapping = record {
+           couniversalMapping = couniversalMapping
+         ; couniquness = couniquness
+     }
+  } where
+   _<=_ = CCC._<=_ ccc
+   <_,_> = CCC.<_,_> ccc
+   _* = CCC._* ccc
+   ε = CCC.ε ccc
+   π = CCC.π ccc
+   π' = CCC.π' ccc
+   isc = CCC.isCCC ccc
+   *-cong = IsCCC.*-cong (CCC.isCCC ccc)
+   ε' :  (a : Obj A) → Hom A (FObj (F_b A ccc b) (a <= b)) a
+   ε' a = ε
+   solution :  { b' : Obj A} {a : Obj A} → Hom A (FObj (F_b A ccc b) a) b' → Hom A a (b' <= b)
+   solution f = f *
+   couniversalMapping : {b = b₁ : Obj A} {a : Obj A}
+            {f : Hom A (FObj (F_b A ccc b) a) b₁} →
+            A [ A [ ε' b₁ o FMap (F_b A ccc b) (solution f) ] ≈ f ]
+   couniversalMapping {c} {a} {f} = IsCCC.e4a isc
+   couniquness :  {b = b₁ : Obj A} {a : Obj A}
+            {f : Hom A (FObj (F_b A ccc b) a) b₁} {g : Hom A a (b₁ <= b)} →
+            A [ A [ ε' b₁ o FMap (F_b A ccc b) g ] ≈ f ] → A [ solution f ≈ g ]
+   couniquness {c} {a} {f} {g} eq = begin
+                 f *
+             ≈↑⟨ *-cong eq ⟩
+                  ( ε o FMap (F_b A ccc b) g ) *
+             ≈⟨⟩
+                  ( ε o < ( g o π ) , π' > ) *
+             ≈⟨ IsCCC.e4b isc  ⟩
+                  g 
+             ∎ 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 1 ( c ^ b ) ≅ Hom A b c
@@ -299,7 +371,7 @@
 hom→CCC A h = record {
          1  = 1
        ; ○ = ○
-       ; _∧_ = _/\_
+       ; _∧_ = _∧_
        ; <_,_> = <,>
        ; π = π
        ; π' = π'
@@ -312,21 +384,21 @@
          1 = one h
          ○ : (a : Obj A ) → Hom A a 1 
          ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj
-         _/\_ : Obj A → Obj A → Obj A   
-         _/\_ a b = _*_ h a b
-         <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b)  
+         _∧_ : Obj A → Obj A → Obj A   
+         _∧_ a b = _*_ h a b
+         <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a ∧ b)  
          <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
-         π : {a b : Obj A } → Hom A (a /\ b) a 
+         π : {a b : Obj A } → Hom A (a ∧ b) a 
          π {a} {b} =  proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
-         π' : {a b : Obj A } → Hom A (a /\ b) b  
+         π' : {a b : Obj A } → Hom A (a ∧ b) b  
          π' {a} {b} =  proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
          _<=_ : (a b : Obj A ) → Obj A 
          _<=_ = _^_ h
-         _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b) 
+         _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
          _* =  ≅← ( ccc-3 (isCCChom h ) )
-         ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a 
+         ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
          ε {a} {b} =  ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) 
-         isCCC : CCC.IsCCC A 1 ○ _/\_ <,> π π' _<=_ _* ε 
+         isCCC : CCC.IsCCC A 1 ○ _∧_ <,> π π' _<=_ _* ε 
          isCCC = record {
                e2  = e2
              ; e3a = e3a
@@ -389,7 +461,7 @@
                   ≈⟨⟩
                     g 
                   ∎ where open ≈-Reasoning A
-               e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } →  A [ <,> ( A [ π o h ] ) ( A [ π' o h  ] )  ≈ h ]
+               e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } →  A [ <,> ( A [ π o h ] ) ( A [ π' o h  ] )  ≈ h ]
                e3c {a} {b} {c} {f} = begin
                    <,> (  π o f  ) (  π' o f   )
                   ≈⟨⟩
@@ -414,7 +486,7 @@
                   ≈⟨⟩
                       <,> f'  g' 
                   ∎ where open ≈-Reasoning A
-               e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } →  A [ A [ ε o ( <,> ( A [ (k *) o π ] )   π')  ] ≈ k ]
+               e4a : {a b c : Obj A} → { k : Hom A (c ∧ b) a } →  A [ A [ ε o ( <,> ( A [ (k *) o π ] )   π')  ] ≈ k ]
                e4a {a} {b} {c} {k} =  begin
                       ε o ( <,> ((k *)  o π  ) π' )
                   ≈⟨⟩
@@ -434,7 +506,7 @@
                   ≈⟨ iso←  (ccc-3 (isCCChom h))  ⟩
                       k
                   ∎ where open ≈-Reasoning A
-               *-cong  : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
+               *-cong  : {a b c : Obj A} {f f' : Hom A (a ∧ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
                *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
 
 open import Category.Sets
@@ -448,7 +520,7 @@
 sets {l} = record {
          1  = One'
        ; ○ = λ _ → λ _ → OneObj'
-       ; _∧_ = _/\_
+       ; _∧_ = _∧_
        ; <_,_> = <,>
        ; π = π
        ; π' = π'
@@ -461,21 +533,21 @@
          1 = One' 
          ○ : (a : Obj Sets ) → Hom Sets a 1
          ○ a = λ _ → OneObj'
-         _/\_ : Obj Sets → Obj Sets → Obj Sets
-         _/\_ a b = a ∧ b
-         <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a /\ b)
+         _∧_ : Obj Sets → Obj Sets → Obj Sets
+         _∧_ a b =  a /\  b
+         <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b)
          <,> f g = λ x → ( f x , g x )
-         π : {a b : Obj Sets } → Hom Sets (a /\ b) a
+         π : {a b : Obj Sets } → Hom Sets (a ∧ b) a
          π {a} {b} =  proj₁ 
-         π' : {a b : Obj Sets } → Hom Sets (a /\ b) b
+         π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b
          π' {a} {b} =  proj₂ 
          _<=_ : (a b : Obj Sets ) → Obj Sets
          a <= b  = b → a
-         _* : {a b c : Obj Sets } → Hom Sets (a /\ b) c → Hom Sets a (c <= b)
+         _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b)
          f * =  λ x → λ y → f ( x , y )
-         ε : {a b : Obj Sets } → Hom Sets ((a <= b ) /\ b) a
+         ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a
          ε {a} {b} =  λ x → ( proj₁ x ) ( proj₂ x )
-         isCCC : CCC.IsCCC Sets 1 ○ _/\_ <,> π π' _<=_ _* ε
+         isCCC : CCC.IsCCC Sets 1 ○ _∧_ <,> π π' _<=_ _* ε
          isCCC = record {
                e2  = e2
              ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
@@ -498,19 +570,19 @@
                 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
                     Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
                 e3b = refl
-                e3c : {a b c : Obj Sets} {h : Hom Sets c (a /\ b)} →
+                e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} →
                     Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
                 e3c = refl
                 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
                     Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
                 π-cong refl refl = refl
-                e4a : {a b c : Obj Sets} {h : Hom Sets (c /\ b) a} →
+                e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} →
                     Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
                 e4a = refl
                 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
                     Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
                 e4b = refl
-                *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a /\ b) c} →
+                *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl