Cartesian Closed Category

Menu Menu

top Agda による圏論入門


Deduction Theorem

examples/deductive.agda
Positive logic は圏A上に構成された論理で以下の対象と射を持ちます。対象は命題で、射は推論だったのを思い出します。

真な命題

         ⊤ : Obj A 

真な命題は何からでも推論できる。

         ○ : (a : Obj A ) → Hom A a ⊤ 

積の対象と、積の構築と射影の推論

         _∧_ : Obj A → Obj A → Obj A   
         <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
         π : {a b : Obj A } → Hom A (a ∧ b) a 
         π' : {a b : Obj A } → Hom A (a ∧ b) b  

関数型とカーリー化と反カーリー化の推論

         _<=_ : (a b : Obj A ) → Obj A 
         _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
         ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 

これを record にまとめます。

    record PositiveLogic {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
         field
             ⊤ : Obj A 
             ○ : (a : Obj A ) → Hom A a ⊤ 
             _∧_ : Obj A → Obj A → Obj A   
             <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
             π : {a b : Obj A } → Hom A (a ∧ b) a 
             π' : {a b : Obj A } → Hom A (a ∧ b) b  
             _<=_ : (a b : Obj A ) → Obj A 
             _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
             ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 

このPositiveLogic上で、以下の Deduction Theorem が成立します。

  もし、a を仮定した証明(射) b → c があったら、それは (a ∧ b )→ c という証明に変換できる

証明の構成は5つの場合にわかれます。

  open PositiveLogic L
  _・_ = _[_o_] A
  
  -- 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
     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 * )

data の : の前は固定入力、: の後は出力であり、出力の方は、それぞれのケースにある引数から自由に作ることができます。i は a を使わずに証明できる場合。ii は a そのものだった時。iii は二つの証明を積で合成した場合。iv は証明の結合。そして、v は関数適用の場合です。data なので、最後はψである必要があります。

List などと同様に、i-v を使って、証明 ψ を構築していくわけです。引数のHom A b cに証明が生成されます。

積の結合則を証明しておきます。

 
  α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
  α = < π  ・ π   , < π'  ・ π  , π'  > >

a を仮定した証明とは、

    ( x : Hom A ⊤ a ) 

を入力とした射、

    {z : Hom A b c }  ( y  : φ {a} x z )

のことです。

  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

という関数が Deduction Theorem に相当します。

y はψを使って構成されているので、C-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 ψ  ・ α ) *


Cartesian Closed Category

CCC は Positive logic のように teminal object と積と application (関数適用)を持つ圏です。

圏で射の結合法則が成立することを以下のようにHom Setで記述できます。

    (0) (Hom A c d  o Hom A c b ) o Hom A a b ≅  Hom A c d  o ( Hom A c b  o Hom A b a )

CCC では追加された終対象、積、適用に対して以下の性質が成立しているものです。

    (1) Hom A a 1 ≅ {*}
    (2) Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
    (3) Hom A a (c ^ b) ≅ Hom A (a × b) c

1への射は唯一つしかありません。積への射は二つの射の直積に対応します。(3)は f (x , y) を (f x) y と考える Curry 化に対応します。逆に対象の関数適用は直積からの射で定義されるわけです。

examples/CCChom.agda
この三つの式は圏で定義してしまう方が楽です。つまり{*}を対象一つの圏として定義します。

    data One  : Set where
          OneObj : One   -- () in Haskell ( or any one object set )
        OneCat : Category Level.zero Level.zero Level.zero
        OneCat = record {
            Obj  = One ;
            Hom = λ a b →   One  ;
            _o_ =  λ{a} {b} {c} x y → OneObj ;
            _≈_ =  λ x y → x ≡ y ;
            Id  =  λ{a} → OneObj ;
            isCategory  =  ...

(1),(2),(3) は、本来は natural iso つまり、射の合成に関する可換性も要求します。必要な1対1を以下のように定義します。

    record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
              :  Set ( c₁  ⊔  c₂ ⊔ ℓ ⊔  c₁'  ⊔  c₂' ⊔ ℓ' ) where
          field
               ≅→ :  Hom A a b   → Hom B a' b'
               ≅← :  Hom B a' b' → Hom A a b
               iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
               iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
               cong→ : {f g : Hom A a b }  → A [ f ≈ g ] →  B [ ≅→ f ≈ ≅→ g ]
               cong← : {f g : Hom B a' b'} → B [ f ≈ g ] →  A [ ≅← f ≈ ≅← g ]

結局、(1)-(3)と可換性は以下のようになります。

    record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (1 : Obj A) 
              ( _*_ : Obj A → Obj A → Obj A  ) ( _^_ : Obj A → Obj A → Obj A  ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
         field
           ccc-1 : {a : Obj A} {b c : Obj OneCat}   →  --   Hom A a 1 ≅ {*}
                              IsoS A OneCat a 1 b c
           ccc-2 : {a b c : Obj A} →  --  Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
                              IsoS A (A × A)  c (a * b) (c , c ) (a , b )
           ccc-3 : {a b c : Obj A} →  -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
                              IsoS A A  a (c ^ b) (a * b) c
           nat-2 : {a b c  : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) }
                     → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈  IsoS.≅→ ccc-2 ( A [ f o g ] ) ]
           nat-3 : {a b c : Obj A} → { k : Hom A c (a ^ b ) } → A [ A [  IsoS.≅→ (ccc-3) (id1 A (a ^ b)) o
                        (IsoS.≅← (ccc-2 ) (A [ k o (proj₁ ( IsoS.≅→ ccc-2  (id1 A (c *  b)))) ] ,
                            (proj₂ ( IsoS.≅→ ccc-2  (id1 A (c *  b) ))))) ] ≈ IsoS.≅→ (ccc-3 ) k ]
    record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
         field
           one : Obj A
           _*_ : Obj A → Obj A → Obj A
           _^_ : Obj A → Obj A → Obj A  
           isCCChom : IsCCChom A one   _*_ _^_


Equaltional な CCC の定義

Hom Set を使わないでCCCを等式的に定義するには以下のようにします。

これは Positive Logic にぴったり対応しています。

examples/CCC.agda

    record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
             ( 1 : Obj A )
             ( ○ : (a : Obj A ) → Hom A a 1 )
              ( _∧_ : Obj A → Obj A → Obj A  ) 
              ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  ) 
              ( π : {a b : Obj A } → Hom A (a ∧ b) a ) 
              ( π' : {a b : Obj A } → Hom A (a ∧ b) b ) 
              ( _<=_ : (a b : Obj A ) → Obj A ) 
              ( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) ) 
              ( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a )
                 :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
     field
       -- cartesian
       e2  : {a : Obj A} → ∀ { f : Hom A a 1 } →  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 ]
       π-cong :  {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ]  → A [ g ≈ g' ]  →  A [ < f , g >  ≈ < f' , g' > ] 
       -- closed
       e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } →  A [ A [ ε o < A [ (h *) o π ]  ,  π' > ] ≈ h ]
       e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]
       *-cong :  {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ]  → A [  f *  ≈  f' * ] 

定義された必要な射と対象がe2からe4までの性質を満たす必要があります。e1 は圏の

    associative : {A B C D : Obj} {f : Hom C D}  {g : Hom B C} {h : Hom A B}
                                  → (f o (g o h)) ≈ ((f o g) o h)

です。

    record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
         field
             1 : Obj A 
             ○ : (a : Obj A ) → Hom A a 1 
             _∧_ : Obj A → Obj A → Obj A   
             <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
             π : {a b : Obj A } → Hom A (a ∧ b) a 
             π' : {a b : Obj A } → Hom A (a ∧ b) b  
             _<=_ : (a b : Obj A ) → Obj A 
             _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
             ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
             isCCC : IsCCC A 1 ○ _∧_ <_,_> π π' _<=_ _* ε 

あとは、この二つの定義が同等であることを示します。

    CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A
    CCC→hom A c = record {
           one = CCC.1 c
         ; _*_ = CCC._∧_ c 
         ; _^_ = CCC._<=_ c
         ; isCCChom = record {
                ccc-1 =  λ {a} {b} {c'} → record {   ≅→ =  c101  ; ≅← = c102  ; iso→  = c103 {a} {b} {c'} ; iso←  = c104 ; cong← = c105 ; cong→ = c106 }
              ; ccc-2 =  record {   ≅→ =  c201 ; ≅← = c202 ; iso→  = c203 ; iso←  = c204  ; cong← = c205; cong→ = c206 }
              ; ccc-3 =   record {   ≅→ =  c301 ; ≅← = c302 ; iso→  = c303 ; iso←  = c304 ; cong← = c305 ; cong→ = c306 }
              ; nat-2 = nat-2 ; nat-3 = nat-3
            }
   }

量が多いわけですが、

      c101 : {a : Obj A} → Hom A a (CCC.1 c) → Hom OneCat OneObj OneObj
      c101 _  = OneObj

一つ一つは簡単です。

      c303 : { c₁ a b  : Obj A} →  {f : Hom A ((c CCC.∧ a) b) c₁} → A [  (c301 ( c302 f ))  ≈ f ]
      c303 = IsCCC.e4a (CCC.isCCC c)

など。反対側は、まず、必要な射と対象を用意する必要があります。

         1 : Obj A 
         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)  
         <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
         π : {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} =  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) 
         _* =  ≅← ( ccc-3 (isCCChom h ) )
         ε : {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 )) 

Hom Set の対応を表す写像が、そのまま必要な射になります。

これを使って、

    hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A
    hom→CCC A h = record {
             1  = 1 ; ○ = ○ ; _∧_ = _∧_ ; <_,_> = <,> ; π = π ; π' = π' ; _<=_ = _<=_ ; _* = _* ; ε = ε
           ; isCCC = isCCC
      } where
             isCCC : CCC.IsCCC A 1 ○ _∧_ <,> π π' _<=_ _* ε 
             isCCC = record {
                   e2  = e2 ; e3a = e3a ; e3b = e3b ; e3c = e3c ; π-cong = π-cong ; e4a = e4a ; e4b = e4b ; *-cong = *-cong
               } where
               e20 : ∀ ( f : Hom OneCat OneObj OneObj ) →  _[_≈_] OneCat {OneObj} {OneObj} f OneObj 
               e20 OneObj = refl
               e2  : {a : Obj A} → ∀ { f : Hom A a 1 } →  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 ) 
                  ≈⟨  ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj}  (
                         λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) )  ⟩
                    ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj
                  ≈⟨⟩
                     ○ a
                  ∎ where open ≈-Reasoning A

という感じで証明していきます。積の場合は

               --
               --             g                 id
               --     a -------------> b * c ------>  b * c
               --
               --     a -------------> b * c ------>  b
               --     a -------------> b * c ------>  c
               --
               cong-proj₁ : {a b c d  : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f  ≈ proj₁ g ]
               cong-proj₁ eq =  proj₁ eq
               cong-proj₂ : {a b c d  : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₂ f  ≈ proj₂ g ]
               cong-proj₂ eq =  proj₂ eq
               e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o <,> f g  ] ≈ f ]
               e3a {a} {b} {c} {f} {g} =  begin
                    π o <,> f g
                  ≈⟨⟩
                     proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o  (≅← (ccc-2 (isCCChom h)) (f , g))
                  ≈⟨ cong-proj₁ (nat-2 (isCCChom h))  ⟩
                     proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a  b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
                  ≈⟨ cong-proj₁  ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
                     proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
                  ≈⟨ cong-proj₁ ( iso→ (ccc-2 (isCCChom h))) ⟩
                     proj₁ ( f , g )
                  ≈⟨⟩
                    f 
                  ∎ where open ≈-Reasoning A

こんな感じで、nat-2 と ccc-2 を使います。


CCCの随伴関手

CCC では

    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 ] ) 

    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) )

の二つの自己関手を作ることができ、これが随伴関手になります。ここでは coUiveralMapping を使います。

    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
         }
      } 

solution は * で、

   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

e4a がsolutionであること、e4b が solution の uniqness に対応します。

   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


Hom A 1 ( c ^ b ) ≅ Hom A b c

    c^b=b<=c : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} →  
                              IsoS A A  (CCC.1 ccc ) (CCC._<=_ ccc  c b) b c

が成立しますが、いがいにめんどくさい。


Sets は CCC

examples/CCCGraph.agda
まず、Sets 内でPositive logic の要素を作ります。割と当たり前。

         1 : Obj Sets 
         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)
         <,> f g = λ x → ( f x , g x )
         π : {a b : Obj Sets } → Hom Sets (a ∧ b) a
         π {a} {b} =  proj₁ 
         π' : {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)
         f * =  λ x → λ y → f ( x , y )
         ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a
         ε {a} {b} =  λ x → ( proj₁ x ) ( proj₂ x )

あとは、e2-e4を示すだけです。

                e2 : {a : Obj Sets} {f : Hom Sets a 1} → Sets [ f ≈ ○ a ]
                e2 {a} {f} = extensionality Sets ( λ x → e20 x )
                  where
                        e20 : (x : a ) → f x ≡ ○ a x
                        e20 x with f x
                        e20 x | OneObj = refl
                e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
                    Sets [ ( Sets [  π  o ( <,> f g)  ] ) ≈ f ]
                e3a = refl
                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)} →
                    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} →
                    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} →
                    Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                *-cong refl = refl

短い。


Graph からCCCの生成

Graph から圏は既に作ってあります。

examples/Graph.agda
Graph に Positive logic の vertex と edge を付け加えます。

 
   data Objs (G : Graph {Level.zero} {Level.zero} ) : Set where    -- formula
      atom : (vertex G) → Objs G
      ⊤ : Objs G
      _∧_ : Objs G → Objs G → Objs G
      _<=_ : Objs G → Objs G → Objs G
   data Arrow (G : Graph ) :  Objs G → Objs G → Set where  --- proof
      arrow : {a b : vertex G} →  (edge G) a b → Arrow G (atom a) (atom b)
      ○ : (a : Objs G ) → Arrow G a ⊤
      π : {a b : Objs G } → Arrow G ( a ∧ b ) a
      π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
      ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a
      <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
      _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )

直接証明しないで、Postive Logic で拡張したGraph から圏を作り、それをSetsに写す関手を定義します。Sets は CCC なので Graph から CCC を作ることができたことになります。

Graph から Sets への写像を用意しておきます。(まだ使わないが、Graph から CCC を生成する時用)

   record SM {v : Level} : Set (suc v)  where
      field
        graph : Graph  {v} {v}
        sobj : vertex graph → Set
        smap : { a b : vertex graph } → edge graph a b  → sobj a → sobj b

まず圏を作ります。

   -- positive intutionistic calculus
   PL : (G : SM) → Graph
   PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) }
   DX : (G : SM) → Category  Level.zero Level.zero Level.zero   
   DX G = GraphtoCat (PL G)

関手 CS の fobj と fmap を定義します。この時に、拡張部分を amap に閉じ込めるのが肝です。

   -- open import Category.Sets
   -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
   fobj : {G : SM} ( a  : Objs (graph G) ) → Set
   fobj {G} (atom x) = sobj G x
   fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
   fobj {G} (a <= b) = fobj {G} b → fobj {G} a
   fobj ⊤ = One
   amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
   amap {G} (arrow x) = smap G x
   amap (○ a) _ = OneObj
   amap π ( x , _) = x
   amap π'( _ , x) = x
   amap ε ( f , x ) = f x
   amap < f , g > x = (amap f x , amap g x)
   amap (f *) x = λ y → amap f ( x , y )
   fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
   fmap {G} {a} (id a) = λ z → z
   fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]
   --   CS is a map from Positive logic to Sets
   --    Sets is CCC, so we have a cartesian closed category generated by a graph
   --       as a sub category of Sets
   CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
   FObj (CS G) a  = fobj a
   FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
   isFunctor (CS G) = isf where
       _++_ = Category._o_ (DX G)
       ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
       distr : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
       distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
          adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
              ( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next x g ) (fmap f z )
          adistr eq x = cong ( λ k → amap x k ) eq
       distr {a} {b} {b} {f} {id b} z =  refl
       isf : IsFunctor (DX G) Sets fobj fmap 
       IsFunctor.identity isf = extensionality Sets ( λ x → refl )
       IsFunctor.≈-cong isf refl = refl
       IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 

Functor の性質自体は amap と関係なく証明されます。amap は一つの射に閉じているので分配法則などには影響しません。


Cart Category of CCC and CCC preserving Functor

次は CCC を対象とする圏 Cart を作ります。これは CAT と同じ。

    record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
       field
         cat : Category c₁ c₂ ℓ
         ccc : CCC cat
     
    open CCCObj 
     
    record CCCMap  {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
       field
         cmap : Functor (cat A ) (cat B )
         ccf :  CCC (cat A) → CCC (cat B)
    open import Category.Cat
    open  CCCMap
    open import Relation.Binary.Core
    Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ))
    Cart {c₁} {c₂} {ℓ} = record {
        Obj = CCCObj {c₁} {c₂} {ℓ}
      ; Hom = CCCMap
      ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) }
      ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g
      ; Id  = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x }
      ; isCategory = record {
         isEquivalence = λ {A} {B} → record {
              refl = λ {f} →  let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} 
            ; sym = λ {f} {g}  → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} 
            ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h}  }
         ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_}
         ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f}
         ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i}  → IsCategory.o-resp-≈ ( Category.isCategory CAT) {cat x}{cat y}{cat z} {cmap f} {cmap g} {cmap h} {cmap i}
         ; associative =  λ {a} {b} {c} {d} {f} {g} {h} → let open ≈-Reasoning (CAT) in assoc {cat a} {cat b} {cat c} {cat d} {cmap f} {cmap g} {cmap h}
       }} 

射の同一性は、ccf に関係しません。

       _≈_ = λ {a} {b} f g → cmap f ≃ cmap g

射が同一なら、向こうとこちらのCCCの構造は自動的に対応しているはずです。


Grph Category of Graph and Graph mapping

次は Graph の圏 Grph を作ります。Cart とほとんど同じ。

    record GMap {v v' : Level} (x y : Graph {v} {v'} )  : Set (suc (v ⊔ v') ) where
      field
       vmap : vertex x → vertex y
       emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)

open GMap

open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )

data [_]_==_ {c₁ c₂ } (C : Graph {c₁} {c₂} ) {A B : vertex C} (f : edge C A B)

     : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ )) where
  mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g

_=m=_ : ∀ {c₁ c₂ } {C D : Graph {c₁} {c₂} }
    → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁))

_=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f

_&_ : {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'} = record {

    Obj = Graph {v} {v'}
  ; Hom = GMap {v} {v'}
  ; _o_ = _&_
  ; _≈_ = _=m=_
  ; Id  = record { vmap = λ y → y ; emap = λ f → f }
  ; isCategory = record {
       isEquivalence = λ {A} {B} →  ise 
     ; identityL = λ e → mrefl refl
     ; identityR =  λ e → mrefl refl
     ; o-resp-≈ = m--resp-≈ 
     ; associative = λ e → mrefl refl
   }}  where
       msym : {v v' : Level} {x y : Graph {v} {v'} }  { f g : GMap x y } → f =m= g → g =m= f
       msym {_} {_} {x} {y} f=g f = lemma ( f=g f ) where
            lemma  : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f
            lemma (mrefl Ff≈Gf) = mrefl  (sym  Ff≈Gf)
       mtrans : {v v' : Level} {x y : Graph {v} {v'} }  { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
       mtrans {_} {_} {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
           lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f}  → [ y ] p == q → [ y ] q == r → [ y ] p == r
           lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv  eqv₁ )
       ise : {v v' : Level} {x y : Graph {v} {v'}}  → IsEquivalence {_} {suc v ⊔ suc v' } {_} ( _=m=_  {v} {v'}  {x} {y}) 
       ise  = record {
          refl =  λ f → mrefl refl
        ; sym = msym
        ; trans = mtrans
          }
       m--resp-≈ : {v v' : Level} {A B C : Graph {v} {v'} }  
           {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
       m--resp-≈ {_} {_} {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
          lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
            lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) →
                [ B ] ϕ  == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
            lemma _ _ _ (mrefl refl) (mrefl refl) = mrefl refl


CCC → Grph Forgetful functor

CCC から Graph への忘却関手です。CAT の等式をそのまま使います。

    ≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
          → { f f'   : Hom B a b }
          → { g g' : Hom B a' b' }
          → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g'
    ≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'}  (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin
                 f'
              ≈↑⟨ f=f' ⟩
                 f
              ≈⟨ eqv  ⟩
                 g
              ≈⟨ g=g' ⟩
                 g'
              ∎  )
 

最後に、圏の射の等式を Sets の等式になおす必要があるので、それは仮定に入れておきます。
 
    fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grph {c₁} {c₂})
    fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
    fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b )
    fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
    UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) →  {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g  )
        → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂})
    FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡  ) a = fobj a
    FMap (UX ≈-to-≡)  f =  fmap f
    isFunctor (UX {c₁} {c₂} {ℓ}  ≈-to-≡)  = isf where
      -- if we don't need ≈-cong ( i.e.   f ≈ g → UX f =m= UX g ), all lemmas are not necessary
      open import HomReasoning
      isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap
      IsFunctor.identity isf {a} {b} {f} e = mrefl refl 
      IsFunctor.distr isf f = mrefl refl
      IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = lemma (extensionality Sets ( λ z → lemma4 (
                   ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
              ))) (eq e) where
          lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
          lemma4 (refl eqv) = refl 
          lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
          lemma refl (refl eqv) = mrefl ( ≈-to-≡ (cat b) eqv )


Generator

Graph から CCC の生成はやってあるので、あとはその uniqunessを示せばよいだけですが、まだ、やってません。


Shinji KONO / Thu May 9 10:09:47 2019