view CCCGraph.agda @ 822:4c0580d9dda4

from cart to graph, hom equality to set equality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 May 2019 21:16:58 +0900
parents fbbc9c03bfed
children f57c9603d989
line wrap: on
line source

open import Level
open import Category 
module CCCgraph where

open import HomReasoning
open import cat-utility
open import Data.Product renaming (_×_ to _/\_  ) hiding ( <_,_> )
open import Category.Constructions.Product
open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import CCC

open Functor

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

open import Category.Sets

-- Sets is a CCC

postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂

data One {l : Level}  : Set l where
  OneObj : One   -- () in Haskell ( or any one object set )

sets : {l : Level } → CCC (Sets {l})
sets {l} = record {
         1  = One
       ; ○ = λ _ → λ _ → OneObj
       ; _∧_ = _∧_
       ; <_,_> = <,>
       ; π = π
       ; π' = π'
       ; _<=_ = _<=_
       ; _* = _*
       ; ε = ε
       ; isCCC = isCCC
  } where
         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 )
         isCCC : CCC.IsCCC Sets 1 ○ _∧_ <,> π π' _<=_ _* ε
         isCCC = record {
               e2  = e2
             ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
             ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
             ; e3c = e3c
             ; π-cong = π-cong
             ; e4a = e4a
             ; e4b = e4b
             ; *-cong = *-cong
           } where
                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

module ccc-from-graph where

   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
   open import discrete
   open graphtocat 

   open Graph

   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 )

   data one {v : Level} {S : Set v} : Set v where
             elm : (x : S ) → one 

   iso→ : {v : Level} {S : Set v} → one → S
   iso→ (elm x) = x

   data iso← {v : Level} {S : Set v} : (one {v} {S} ) → S → Set v where
       elmeq : {x : S} →  iso←  ( elm x ) x

   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso← x a → iso→ x ≡ a
   iso-left (elm x) .x elmeq = refl

   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x ) 
   iso-right (elm x) = elmeq

--   record one {v : Level} {S : Set v} : Set (suc v) where
--      field
--         elm : S
--
--   iso→ : {v : Level} {S : Set v} → one {v} {S} → One {Level.zero} → S
--   iso→ x OneObj = one.elm x
--   iso← : {v : Level} {S : Set v} → one {v} {S} → S → One {Level.zero}
--   iso← x y = OneObj
--
--   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso→ x ( iso← x a ) ≡ a
--   iso-left x a =  {!!}
--
--   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x OneObj ) ≡ OneObj
--   iso-right x =  refl

   record one' {v : Level} {S : Set v} : Set (suc v) where
     field
        elm' : S
        iso→' : One {Level.zero} → S
        iso←' : S → One {Level.zero}
        iso-left' : iso→' ( iso←' elm' ) ≡ elm'
        iso-right' : iso←' ( iso→' OneObj ) ≡ OneObj

   tmp : {v : Level} {S : Set v} → one {v} {S}  → one' {v} {S}
   tmp x = record {
         elm' = iso→ x
       ; iso→' = λ _ → iso→ x
       ; iso←' = λ _ → OneObj
       ; iso-left' = refl
       ; iso-right' = refl
     }
     


   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

   open SM

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

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

---
---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
---
---     CCC ( SC (CS G)) Sets   have to be proved
---  SM can be eliminated if we have
---    sobj (a : vertex g ) → {a}              a set have only a
---    smap (a b : vertex g ) → {a} → {b}


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} 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}
   }} where
      cart-refl : {A B : CCCObj {c₁} {c₂} {ℓ} } → { x : CCCMap A B } → {a b : Obj ( cat A ) } → (f : Hom ( cat A ) a b)  →  [ cat B ] FMap (cmap x) f ~ FMap (cmap x) f
      cart-refl {A} {B} {x} {a} {b} f = [_]_~_.refl  ( IsFunctor.≈-cong (isFunctor ( cmap x ))
            (  IsEquivalence.refl (IsCategory.isEquivalence (Category.isCategory ( cat A  )))))
      _・_ : { A B C : CCCObj {c₁} {c₂} {ℓ} } → ( f : CCCMap B C  ) → ( g : CCCMap A B  ) → CCCMap A C  
      _・_ {A} {B} {C} f g = record { cmap = F ; ccf = ccmap }  where
         F : Functor (cat A) (cat C)
         F = (cmap f) ○ ( cmap g )
         ccmap :  CCC (cat A) → CCC (cat C)
         ccmap ca = ccf f ( ccf g (ccc A ))

open import discrete
open Graph

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 _=m=_ {v v' : Level} {x y : Graph {v} {v'}} ( f g : GMap x y ) :  Set (v ⊔ v'  ) where
     mrefl : ( vmap f ≡ vmap g ) → ( {a b : vertex x} → { e : edge x a b } → emap f e  ≅ emap g e ) → f =m= g

_&_ :  {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 ) }

Grp : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (v ⊔ v')
Grp {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 {v} {v'} {A} {B} 
     ; identityL = mrefl refl refl
     ; identityR =  mrefl refl refl
     ; o-resp-≈ = m--resp-≈ 
     ; associative = mrefl refl refl
   }}  where
       msym : {v v' : Level} {x y : Graph {v} {v'} } { f g : GMap x y } → f =m= g → g =m= f
       msym (mrefl refl eq ) = mrefl refl ( ≅-sym eq ) 
       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 (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( ≅-trans eq eq1 ) 
       ise : {v v' : Level} {x y : Graph {v} {v'}} → IsEquivalence {_} {v ⊔ v'} {_} ( _=m=_ {v} {v'} {x} {y} )
       ise  = record {
          refl =  λ {x} → mrefl refl refl
        ; sym = msym
        ; trans = mtrans
          }
       m--resp-≈ : {v : Level} {A B C : Graph {v} } {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
       m--resp-≈ {_} {_} {_} {_} {f} {g} {h} {i}  (mrefl refl eq ) (mrefl refl eq1 ) = mrefl refl ( λ {a} {b} {e} →  begin
                  emap h (emap f e)
               ≅⟨ ≅-cong ( λ k → emap h k ) eq  ⟩
                  emap h (emap g e)
               ≅⟨ eq1  ⟩
                  emap i (emap g e)
               ∎  )
               where open Relation.Binary.HeterogeneousEquality.≅-Reasoning 
       assoc-≈ : {v v' : Level} {A B C D : Graph {v} {v'} } {f : GMap C D} {g : GMap B C} {h : GMap A B} → ( f & ( g & h ) ) =m= ( (f & g ) & h )
       assoc-≈ = mrefl refl refl

--- Forgetful functor

fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grp {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 (Grp {c₁} {c₂}) ( fobj a ) ( fobj b )
fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }

≃-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'
          ∎  )
  

UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂})
FObj (UX {c₁} {c₂} {ℓ}) a = fobj a
FMap UX f =  fmap f
isFunctor (UX {c₁} {c₂} {ℓ}) = isf where
  open import HomReasoning
  lemma0 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a b : Obj B} → [_]_~_ B  (id1 B a) (id1 B b) → a ≡ b 
  lemma0 {A} {B} {f} {g} (refl eqv) = refl
  lemma03 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → [_]_~_ B  (FMap f ( id1 A a)) (FMap g ( id1 A a)) → FObj f a ≡ FObj g a 
  lemma03 {A} {B} {f} {g} eq = lemma0 {A} {B} {f} {g} ( ≃-cong B eq (IsFunctor.identity (Functor.isFunctor (f)))(IsFunctor.identity (Functor.isFunctor (g)))  )
  lemma01 : {A B : Category c₁ c₂ ℓ } { f g : Functor A B } → {a : Obj A} → f ≃ g  →  FObj f a ≡ FObj g a 
  lemma01 {A} {B} {f} {g} {a}  eq = lemma03 {A} {B} {f} {g} (eq (id1 A a))
  lemma1 : {A B : Obj (Cart {c₁} {c₂} {ℓ}) } { f g : Hom (Cart {c₁} {c₂} {ℓ}) A B }
       → (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ] → vmap (fmap f) ≡ vmap (fmap g)
  lemma1 {a} {b} {f} {g} eq = extensionality Sets ( λ z → lemma01 {cat a} {cat b} {cmap f} {cmap g} eq  )
  lemma20 : {A B : Category c₁ c₂ ℓ }  {a b : Obj A} → ( e : Hom A a b ) → ( g : Functor A B )  → ( f : Hom A a b → Hom B (FObj g a) (FObj g b) ) 
       → B [ f e ≈ FMap g e ] → f e ≅ FMap g e
  lemma20 e g f eq = {!!}
  lemma2 : {A B : Obj (Cart {c₁} {c₂} {ℓ}) } { f g : Hom (Cart {c₁} {c₂} {ℓ}) A B} →
      (Cart {c₁} {c₂} {ℓ}) [ f ≈ g ]  → vmap (fmap f) ≡ vmap (fmap g)  → {a b : vertex (fobj A)} {e : edge (fobj A) a b} → emap (fmap f) e ≅ emap (fmap g) e
  lemma2 {A} {B} {f} {g} eq refl {a} {b} {e} with ( eq e )
  ... | refl {h} eqv =  lemma20 e (cmap g) (FMap (cmap f)) eqv
  isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap
  IsFunctor.identity isf = mrefl refl refl
  IsFunctor.distr isf = mrefl refl refl
  IsFunctor.≈-cong isf {a} {b} {f} {g} eq = mrefl (lemma1 {a} {b} {f} {g} eq ) (lemma2 {a} {b} {f} {g} eq (lemma1 {a} {b} {f} {g} eq ))

---   
---   open ccc-from-graph
---   
---   sm : {v : Level } → Graph {v} → SM {v}
---   SM.graph (sm g) = g
---   SM.sobj (sm  g) = {!!}
---   SM.smap (sm  g) = {!!}
---   
---   HX : {v : Level } ( x : Obj (Grp {v}) ) → Obj (Grp {v})
---   HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ;  ccc = sets } )
---   
---   
---   
---