Mercurial > hg > Members > kono > Proof > category

changeset 929:1e8ed7dedc03

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... simpler level on CCC Graph
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 May 2020 16:26:35 +0900
parents c1222aa20244
children 327abed926d6
files CCCGraph.agda
diffstat 1 files changed, 52 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sun May 10 20:27:36 2020 +0900
+++ b/CCCGraph.agda	Mon May 11 16:26:35 2020 +0900
@@ -1,6 +1,6 @@
 open import Level
 open import Category 
-module CCCgraph  where
+module CCCgraph (c₁ : Level )  where
 
 open import HomReasoning
 open import cat-utility
@@ -21,11 +21,11 @@
 
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-data One {l : Level}  : Set l where
+data One  : Set (suc c₁) where
   OneObj : One   -- () in Haskell ( or any one object set )
 
-sets : {l : Level } → CCC (Sets {l})
-sets {l} = record {
+sets : CCC (Sets {suc c₁})
+sets  = record {
          １  = One
        ; ○ = λ _ → λ _ → OneObj
        ; _∧_ = _∧_
@@ -95,19 +95,19 @@
                 *-cong refl = refl
 
 open import graph
-module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
+module ccc-from-graph  (G : Graph {suc c₁} {suc 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₁  ⊔  c₂ ) 
-   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where                       --- case i
+   data  Arrows  : (b c : Objs ) → Set (suc c₁  )
+   data Arrow :  Objs → Objs → Set (suc 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
@@ -143,7 +143,7 @@
    assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h )
 
    -- positive intutionistic calculus
-   PL :  Category  c₁  (c₁ ⊔ c₂) (c₁ ⊔ c₂)
+   PL :  Category  (suc c₁) (suc c₁)  (suc c₁ )
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
@@ -175,7 +175,7 @@
    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) 
    
-   fobj :  ( a  : Objs  ) → Set (c₁ ⊔ c₂ )
+   fobj :  ( a  : Objs  ) → Set (suc c₁ )
    fobj  (atom x) = ( y : vertex G ) → C y x
    fobj ⊤ = One
    fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
@@ -197,7 +197,7 @@
 --    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₁ ⊔ c₂ })
+   CS :  Functor PL (Sets {suc c₁})
    FObj CS a  = fobj  a
    FMap CS {a} {b} f = fmap  {a} {b} f
    isFunctor CS = isf where
@@ -226,15 +226,15 @@
 ---    smap (a b : vertex g ) → {a} → {b}
 
 
-record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+record CCCObj  : Set (suc c₁) where
    field
-     cat : Category c₁ c₂ ℓ
+     cat : Category c₁ c₁  c₁ 
      ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g
      ccc : CCC cat
  
 open CCCObj 
  
-record CCCMap  {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+record CCCMap  (A B : CCCObj ) : Set (suc c₁ ) where
    field
      cmap : Functor (cat A ) (cat B )
      ccf :  CCC (cat A) → CCC (cat B)
@@ -244,9 +244,9 @@
 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₂} {ℓ}
+Cart :  Category (suc c₁) (suc c₁) (suc c₁)
+Cart = record {
+    Obj = CCCObj 
   ; 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
@@ -265,7 +265,7 @@
 open import graph
 open Graph
 
-record GMap {c₁ c₂ : Level} (x y : Graph {c₁} {c₂} )  : Set (c₁ ⊔ c₂ ) where
+record GMap  (x y : Graph {c₁} {c₁} )  : Set (suc c₁) where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
@@ -274,21 +274,21 @@
 
 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
+data [_]_==_ (C : Graph {c₁} {c₁} ) {A B : vertex C} (f : edge C A B)
+     : ∀{X Y : vertex C} → edge C X Y → Set (suc 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 D : Graph {c₁} {c₁} } 
+    → (F G : GMap C D) → Set (suc  c₁)
 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
 
-_&_ :  {c₁ c₂ : Level} {x y z : Graph {c₁} {c₂}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
+_&_ :  {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 : {c₁ c₂ : Level} → Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (suc ( c₁ ⊔ c₂))
-Grph {c₁} {c₂} = record {
-    Obj = Graph {c₁} {c₂}
-  ; Hom = GMap {c₁} {c₂}
+Grph :  Category (suc c₁)  (suc c₁) (suc c₁)
+Grph  = record {
+    Obj = Graph {c₁} {c₁}
+  ; Hom = GMap 
   ; _o_ = _&_
   ; _≈_ = _=m=_
   ; Id  = record { vmap = λ y → y ; emap = λ f → f }
@@ -299,23 +299,23 @@
      ; o-resp-≈ = m--resp-≈ 
      ; associative = λ e → mrefl refl
    }}  where
-       msym : {c₁ c₂ : Level} {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
+       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 : {c₁ c₂ : Level} {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
+       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 : {c₁ c₂ : Level} {x y : Graph {c₁} {c₂}}  → IsEquivalence {_} {suc c₁ ⊔ suc c₂ } {_} ( _=m=_  {c₁} {c₂}  {x} {y}) 
+       ise : {x y : Graph {c₁} {c₁}}  → IsEquivalence {_} {suc c₁ } {_} ( _=m=_ {x} {y}) 
        ise  = record {
           refl =  λ f → mrefl refl
         ; sym = msym
         ; trans = mtrans
           }
-       m--resp-≈ : {c₁ c₂ : Level} {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 =
+       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 ϕ) == π
@@ -323,7 +323,7 @@
 
 --- Forgetful functor
 
-module forgetful  {c₁ c₂ : Level} where
+module forgetful  where
 
   ≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
       → { f f'   : Hom B a b }
@@ -339,12 +339,12 @@
              g'
           ∎  )
   
-  fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂} )  → Obj (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂})
+  fobj : Obj Cart → Obj Grph
   fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
-  fmap :  {a b : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) } → Hom (Cart ) a b → Hom (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}) ( fobj a ) ( fobj b )
+  fmap :  {a b : Obj (Cart   ) } → Hom (Cart ) a b → Hom (Grph  ) ( fobj a ) ( fobj b )
   fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
 
-  UX :  Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}  )
+  UX :  Functor Cart Grph
   FObj UX a = fobj a
   FMap UX f =  fmap f
   isFunctor UX  = isf where
@@ -365,8 +365,8 @@
 open ccc-from-graph.Arrows
 open graphtocat.Chain
 
-ccc-graph-univ :  {c₁ c₂ : Level } → UniversalMapping (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}) (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (forgetful.UX {c₁} {c₂} )
-ccc-graph-univ {c₁} {c₂}  = record {
+ccc-graph-univ :  UniversalMapping Grph Cart forgetful.UX 
+ccc-graph-univ = record {
      F = λ g → csc {!!} ; -- g
      η = λ a → record { vmap = λ y → {!!} ; emap = λ f x y →  next f (x y) } ; -- graphtocat.Chain a ? ?  
      _* = solution ;
@@ -375,21 +375,21 @@
          uniquness = {!!}
       }
   } where
-       open forgetful  {c₁} {c₂}
+       open forgetful  
        open ccc-from-graph
-       csc : Graph {c₁} {c₂} → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
-       csc  g = record { cat = Sets {c₁ ⊔ c₂}  ; ccc = sets {c₁ ⊔ c₂} ; ≡←≈ = λ eq → eq } 
-       cs :  (g : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}) → Functor  (ccc-from-graph.PL g) (Sets {suc (c₁ ⊔ c₂)})
-       cs g = CS g
-       pl :  (g : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} ) → Category _ _ _
+       csc : Graph {suc c₁} {suc c₁} → Obj Cart  
+       csc  g = record { cat = {!!} ; ccc = {!!} ; ≡←≈ = λ eq → eq } 
+       cs :  (g : Graph {suc c₁}{suc c₁} ) → Functor  (ccc-from-graph.PL g) (Sets {suc c₁})
+       cs g = {!!}
+       pl :  (g : Graph {suc c₁} {suc c₁ } ) → Category _ _ _
        pl g = PL g
-       cobj  :   {g : Obj (Grph   {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)})} {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 : Obj (Grph    )} {c : Obj (Cart)} → Hom Grph g (FObj UX c)  → Objs {!!} → Obj (cat c)
+       cobj {g} {c} f (atom x) = vmap f {!!}
        cobj {g} {c} f ⊤ = CCC.１ (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 {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)} )} {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 : 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} {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) = {!!}
@@ -397,7 +397,7 @@
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
        c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!})
        c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!})
-       solution : {g : Obj (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)})} {c : Obj (Cart )} → Hom Grph g (FObj UX c) → Hom (Cart ) {!!} {!!}
-       solution  {g} {c} f = ? -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
+       solution : {g : Obj (Grph  )} {c : Obj (Cart )} → Hom Grph g (FObj UX c) → Hom (Cart ) {!!} {!!}
+       solution  {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }