# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589266608 -32400
# Node ID 98b5fafb1efba105a601ad7314f8a319fe542bb2
# Parent  327abed926d60eed1ba81a2bfebe39b830e26862
...

diff -r 327abed926d6 -r 98b5fafb1efb CCCGraph.agda
--- a/CCCGraph.agda	Mon May 11 16:47:58 2020 +0900
+++ b/CCCGraph.agda	Tue May 12 15:56:48 2020 +0900
@@ -21,7 +21,10 @@
 
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-data One  : Set c₁ where
+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₁})
@@ -95,19 +98,19 @@
                 *-cong refl = refl
 
 open import graph
-module ccc-from-graph  (G : Graph {c₁} {c₁} )  where
+module ccc-from-graph  (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 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 c₂ 
+   data Arrow :  Objs → Objs → Set 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 +146,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  c₂ c₂ c₂ 
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
@@ -175,7 +178,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₁
+   fobj :  ( a  : Objs  ) → Set c₂
    fobj  (atom x) = ( y : vertex G ) → C y x
    fobj ⊤ = One
    fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
@@ -198,9 +201,9 @@
 --       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 = isf where
+   FObj CS a  = {!!} -- fobj  a
+   FMap CS {a} {b} f = {!!} -- fmap  {a} {b} f
+   isFunctor CS = {!!} where -- 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)
@@ -226,15 +229,15 @@
 ---    smap (a b : vertex g ) → {a} → {b}
 
 
-record CCCObj  : Set (suc c₁) where
+record CCCObj  : Set c₃ where
    field
-     cat : Category c₁ 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  (A B : CCCObj ) : Set (suc c₁) where
+record CCCMap  (A B : CCCObj ) : Set c₃ where
    field
      cmap : Functor (cat A ) (cat B )
      ccf :  CCC (cat A) → CCC (cat B)
@@ -244,7 +247,7 @@
 open  CCCMap
 open import Relation.Binary.Core
 
-Cart :  Category (suc c₁) (suc c₁) (suc c₁) 
+Cart :  Category c₃ c₃ c₃ 
 Cart = record {
     Obj = CCCObj 
   ; Hom = CCCMap
@@ -265,7 +268,7 @@
 open import graph
 open Graph
 
-record GMap  (x y : Graph {c₁} {c₁} )  : Set (suc c₁) where
+record GMap  (x y : Graph {c₂} {c₁} )  : Set c₂ where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
@@ -274,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 (suc 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 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 (suc c₁)
+_=m=_ : {C D : Graph {c₂} {c₁} } 
+    → (F G : GMap C D) → Set 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
+_&_ :  {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 (suc c₁) (suc c₁)  (suc c₁) 
+Grph :  Category c₃ c₂  c₂ 
 Grph  = record {
-    Obj = Graph {c₁} {c₁}
+    Obj = Graph {c₂} {c₁}
   ; Hom = GMap 
   ; _o_ = _&_
   ; _≈_ = _=m=_
@@ -299,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 {_} {suc 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
@@ -365,13 +368,13 @@
 open ccc-from-graph.Arrows
 open graphtocat.Chain
 
-Sets0 : Category (suc c₁) c₁ c₁
+Sets0 : Category c₂ c₁ c₁
 Sets0 = Sets {c₁}
 
 ccc-graph-univ :  UniversalMapping Grph Cart forgetful.UX 
 ccc-graph-univ = record {
      F = λ g → csc g ; 
-     η = λ a → record { vmap = λ y → graphtocat.Chain {!!} {!!} {!!} ; emap = λ f x y →  next f (x y) } ; -- graphtocat.Chain a ? ?  
+     η = λ a → record { vmap = λ y →  {!!} ; emap = λ f x →  {!!} } ; -- graphtocat.Chain a ? ?  
      _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
@@ -380,14 +383,14 @@
   } where
        open forgetful  
        open ccc-from-graph
-       csc : Graph {c₁} {c₁} → Obj Cart  
-       csc  g = record { cat = {!!} ; ccc = {!!} ; ≡←≈ = λ eq → eq } 
-       cs :  (g : Graph {c₁}{c₁} ) → Functor  (ccc-from-graph.PL g) (Sets {suc c₁})
-       cs g = {!!}
-       pl :  (g : Graph {c₁} {c₁ } ) → Category _ _ _
+       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₁})
+       cs g = CS g
+       pl :  (g : Graph {c₂} {c₁ } ) → Category _ _ _
        pl g = PL g
-       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 : 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.１ (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) 
@@ -400,7 +403,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  )} {c : Obj (Cart )} → Hom Grph g (FObj UX c) → Hom (Cart ) {!!} {!!}
+       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 = {!!} }