changeset 932:f19425b54aba

introduce detailed level on CCCGraph
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 May 2020 22:26:09 +0900
parents 98b5fafb1efb
children e702aa8be9dd
files CCCGraph.agda
diffstat 1 files changed, 47 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Tue May 12 15:56:48 2020 +0900
+++ b/CCCGraph.agda	Tue May 12 22:26:09 2020 +0900
@@ -1,6 +1,6 @@
 open import Level
 open import Category 
-module CCCgraph (c₁ : Level )  where
+module CCCgraph  where
 
 open import HomReasoning
 open import cat-utility
@@ -21,13 +21,10 @@
 
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-c₂ = suc c₁
-c₃ = suc c₂
-
 data One  {c : Level } : Set c where
   OneObj : One   -- () in Haskell ( or any one object set )
 
-sets : CCC (Sets {c₁})
+sets : {c : Level } → CCC (Sets {c})
 sets  = record {
          1  = One
        ; ○ = λ _ → λ _ → OneObj
@@ -97,20 +94,21 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
+
 open import graph
-module ccc-from-graph  (G : Graph {c₂} {c₁} )  where
+module ccc-from-graph {c₁ c₂ : Level }  (G : Graph {c₁} {c₂})  where
 
    open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
    open Graph
 
-   data Objs : Set c₂ where
+   data Objs : Set (suc c₁) where
       atom : (vertex G) → Objs 
       ⊤ : Objs 
       _∧_ : Objs  → Objs  → Objs 
       _<=_ : Objs → Objs → Objs 
 
-   data  Arrows  : (b c : Objs ) → Set c₂ 
-   data Arrow :  Objs → Objs → Set c₂  where                       --- case i
+   data  Arrows  : (b c : Objs ) → Set (suc c₁  ⊔  c₂)
+   data Arrow :  Objs → Objs → Set (suc c₁  ⊔ c₂)  where                       --- case i
       arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
       π : {a b : Objs } → Arrow ( a ∧ b ) a
       π' : {a b : Objs } → Arrow ( a ∧ b ) b
@@ -146,7 +144,7 @@
    assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h )
 
    -- positive intutionistic calculus
-   PL :  Category  c₂ c₂ c₂ 
+   PL :  Category  (suc c₁) (suc c₁  ⊔ c₂) (suc c₁  ⊔ c₂)
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
@@ -173,12 +171,14 @@
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂
 
+   open import Data.List
+
    C = graphtocat.Chain G
 
    tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
-   tr f x y  = graphtocat.next f (x y) 
+   tr f x y = graphtocat.next f (x y) 
    
-   fobj :  ( a  : Objs  ) → Set c₂
+   fobj :  ( a  : Objs  ) → Set (c₁  ⊔ c₂)
    fobj  (atom x) = ( y : vertex G ) → C y x
    fobj ⊤ = One
    fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
@@ -186,7 +186,7 @@
 
    fmap :  { a b : Objs  } → Hom PL a b → fobj  a → fobj  b
    amap :  { a b : Objs  } → Arrow  a b → fobj  a → fobj  b
-   amap  (arrow x) =  tr x
+   amap  (arrow x) y =  tr x y -- tr x
    amap π ( x , y ) = x 
    amap π' ( x , y ) = y
    amap ε (f , x ) = f x
@@ -200,10 +200,10 @@
 --    Sets is CCC, so we have a cartesian closed category generated by a graph
 --       as a sub category of Sets
 
-   CS :  Functor PL (Sets {c₁})
-   FObj CS a  = {!!} -- fobj  a
-   FMap CS {a} {b} f = {!!} -- fmap  {a} {b} f
-   isFunctor CS = {!!} where -- isf where
+   CS :  Functor PL (Sets {c₁ ⊔ c₂})
+   FObj CS a  = fobj  a
+   FMap CS {a} {b} f = fmap  {a} {b} f
+   isFunctor CS = isf where
         _+_ = Category._o_ PL
         ++idR = IsCategory.identityR ( Category.isCategory PL )
         distr : {a b c : Obj PL}  { f : Hom PL a b } { g : Hom PL b c } → (z : fobj  a ) → fmap (g + f) z ≡ fmap g (fmap f z)
@@ -229,15 +229,15 @@
 ---    smap (a b : vertex g ) → {a} → {b}
 
 
-record CCCObj  : Set c₃ where
+record CCCObj {c₁ c₂ ℓ : Level}  : Set  (suc (ℓ ⊔ (c₂ ⊔ c₁))) where
    field
-     cat : Category c₂ c₁  c₁ 
+     cat : Category c₁ c₂ ℓ
      ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g
      ccc : CCC cat
  
 open CCCObj 
  
-record CCCMap  (A B : CCCObj ) : Set c₃ where
+record CCCMap {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (A : CCCObj {c₁} {c₂} {ℓ} ) (B : CCCObj {c₁′} {c₂′}{ℓ′} ) : Set (suc (ℓ′ ⊔ (c₂′ ⊔ c₁′) ⊔ ℓ ⊔ (c₂ ⊔ c₁))) where
    field
      cmap : Functor (cat A ) (cat B )
      ccf :  CCC (cat A) → CCC (cat B)
@@ -247,9 +247,9 @@
 open  CCCMap
 open import Relation.Binary.Core
 
-Cart :  Category c₃ c₃ c₃ 
-Cart = record {
-    Obj = CCCObj 
+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
@@ -268,7 +268,7 @@
 open import graph
 open Graph
 
-record GMap  (x y : Graph {c₂} {c₁} )  : Set c₂ where
+record GMap {c₁ c₂ c₁' c₂' : Level}  (x : Graph {c₁} {c₂} ) (y : Graph {c₁'} {c₂'}  )  : Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂') where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
@@ -277,20 +277,20 @@
 
 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
 
-data [_]_==_ (C : Graph {c₂} {c₁} ) {A B : vertex C} (f : edge C A B)
-     : ∀{X Y : vertex C} → edge C X Y → Set c₂ where
+data [_]_==_ {c₁ c₂ : Level} (C : Graph  {c₁} {c₂}) {A B : vertex C} (f : edge C A B)
+     : ∀{X Y : vertex C} → edge C X Y → Set (c₁ ⊔ c₂ ) where
   mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
 
-_=m=_ : {C D : Graph {c₂} {c₁} } 
-    → (F G : GMap C D) → Set c₂
+_=m=_ : {c₁ c₂ c₁' c₂'  : Level} {C : Graph {c₁} {c₂} } {D : Graph {c₁'} {c₂'} }
+    → (F G : GMap C D) → Set (c₁ ⊔ c₂ ⊔ 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
 
-_&_ :  {x y z : Graph {c₂} {c₁}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
+_&_ :  {c₁ c₂ : Level} {x y z : Graph {c₁} {c₂} } ( 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 :  Category c₃ c₂  c₂ 
-Grph  = record {
-    Obj = Graph {c₂} {c₁}
+Grph : {c₁ c₂ : Level} →  Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
+Grph {c₁} {c₂}  = record {
+    Obj = Graph {c₁} {c₂}
   ; Hom = GMap 
   ; _o_ = _&_
   ; _≈_ = _=m=_
@@ -302,21 +302,21 @@
      ; o-resp-≈ = m--resp-≈ 
      ; associative = λ e → mrefl refl
    }}  where
-       msym : {x y : Graph {c₂} {c₁} }  { f g : GMap x y } → f =m= g → g =m= f
+       msym : {x y : Graph {c₁} {c₂} }  { 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 :  {x y : Graph {c₂} {c₁} }  { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
+       mtrans :  {x y : Graph {c₁} {c₂} }  { 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 : {x y : Graph {c₂} {c₁}}  → IsEquivalence {_} {suc c₁ } {_} ( _=m=_ {x} {y}) 
+       ise : {x y : Graph {c₁} {c₂} }  → IsEquivalence {_} {c₁ ⊔ c₂} {_} ( _=m=_ {_} {_} {_} {_} {x} {y}) 
        ise  = record {
           refl =  λ f → mrefl refl
         ; sym = msym
         ; trans = mtrans
           }
-       m--resp-≈ :  {A B C : Graph {c₂} {c₁} }  
+       m--resp-≈ :  {A B C : Graph {c₁} {c₂} }   
            {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
@@ -368,13 +368,13 @@
 open ccc-from-graph.Arrows
 open graphtocat.Chain
 
-Sets0 : Category c₂ c₁ c₁
-Sets0 = Sets {c₁}
+Sets0 : {c₂ : Level } → Category (suc c₂) c₂ c₂
+Sets0 {c₂} = Sets {c₂}
 
 ccc-graph-univ :  UniversalMapping Grph Cart forgetful.UX 
 ccc-graph-univ = record {
-     F = λ g → csc g ; 
-     η = λ a → record { vmap = λ y →  {!!} ; emap = λ f x →  {!!} } ; -- graphtocat.Chain a ? ?  
+     F = λ g → csc {!!}   ;
+     η = λ a → record { vmap = λ y →  graphtocat.Chain {!!} {!!} {!!}  ; emap = λ f x →  {!!} } ; -- 
      _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
@@ -383,19 +383,19 @@
   } where
        open forgetful  
        open ccc-from-graph
-       csc : Graph {c₂} {c₁} → Obj Cart  
-       csc  g = record { cat = Sets ; ccc = sets ; ≡←≈ = λ eq → eq } 
-       cs :  (g : Graph {c₂}{c₁} ) → Functor  (ccc-from-graph.PL g) (Sets {c₁})
+       csc : {c₁ c₂ : Level}  → Graph {c₂} {c₁}  → Obj Cart  
+       csc {c₁} {c₂}  g = record { cat = Sets {c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } 
+       cs : {c₁ c₂ : Level}  → (g : Graph  {c₁} {c₂} ) → Functor  (ccc-from-graph.PL g) (Sets {_})
        cs g = CS g
-       pl :  (g : Graph {c₂} {c₁ } ) → Category _ _ _
+       pl : {c₁ c₂ : Level}  → (g : Graph {c₁} {c₂} ) → Category _ _ _
        pl g = PL g
-       cobj  :   {g : Obj Grph } {c : Obj Cart} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
+       cobj  :  {g : Obj Grph } {c : Obj Cart} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
        cobj {g} {c} f (atom x) = vmap f x
        cobj {g} {c} f ⊤ = CCC.1 (ccc c)
        cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
-       c-map :  {g : Obj (Grph  )} {c : Obj Cart} {A B : Objs {!!}}
-           → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl {!!}) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
+       c-map :  {g : Obj (Grph  )} {c : Obj Cart} {A B : Objs g} 
+           → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl g) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
        c-map {g} {c} {atom a} {atom x} f y = {!!}
        c-map {g} {c} {⊤} {atom x} f (iv f1 y) = {!!}
        c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!}