Mercurial > hg > Members > kono > Proof > category

changeset 825:8f41ad966eaa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rename discrete
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 May 2019 17:11:33 +0900
parents 878d8643214f
children d1569e80fe0b b8c5f15ee561
files CCCGraph.agda discrete.agda graph.agda limit-to.agda
diffstat 4 files changed, 222 insertions(+), 222 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Thu May 02 11:54:09 2019 +0900
+++ b/CCCGraph.agda	Fri May 03 17:11:33 2019 +0900
@@ -97,7 +97,7 @@
 module ccc-from-graph where
 
    open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
-   open import discrete
+   open import graph
    open graphtocat 
 
    open Graph
@@ -265,10 +265,10 @@
      ; 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}
    }} 
 
-open import discrete
+open import graph
 open Graph
 
-record GMap {v v' w w' : Level} (x : Graph {v} {v'} ) (y : Graph {w} {w'} ) : Set (suc (v ⊔ w) ⊔  v' ⊔ w' ) where
+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)
--- a/discrete.agda	Thu May 02 11:54:09 2019 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,206 +0,0 @@
-open import Category -- https://github.com/konn/category-agda
-open import Level
-
-module discrete where
-
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
-
-record Graph  { v v' : Level } : Set (suc v ⊔ suc v' ) where
-  field
-    vertex : Set v
-    edge : vertex  → vertex → Set v'
-
-module graphtocat where
-
-  open import Relation.Binary.PropositionalEquality 
-
-  data Chain { v v' : Level } ( g : Graph {v} {v'} ) : ( a b : Graph.vertex g ) → Set (v ⊔ v' ) where
-       id : ( a : Graph.vertex g ) → Chain g a a
-       next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain g a b → Chain g a c
-
-  _・_ :  {v v' : Level} { G : Graph {v} {v'} } {a b c : Graph.vertex G } (f : Chain G b c ) → (g : Chain G a b) → Chain G a c
-  id _ ・ f = f
-  (next x f) ・ g = next x ( f ・ g )
-
-  GraphtoCat : {v v' : Level} (G : Graph {v} {v'} )  →  Category  v (v ⊔ v') (v ⊔ v')
-  GraphtoCat G = record {
-            Obj  = Graph.vertex G ;
-            Hom = λ a b →  Chain G a b ;
-            _o_ =  λ{a} {b} {c} x y → x ・ y ;
-            _≈_ =  λ x y → x  ≡ y ;
-            Id  =  λ{a} → id a ;
-            isCategory  = record {
-                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-                    identityL  = identityL; 
-                    identityR  = identityR ; 
-                    o-resp-≈  = o-resp-≈  ; 
-                    associative  = λ{a b c d f g h } → associative  f g h
-               }
-           }  where
-               open Chain
-               obj = Graph.vertex G
-               hom = Graph.edge G
-
-               identityL : {A B : Graph.vertex G} {f : Chain G A B} → (id B ・ f) ≡ f
-               identityL = refl
-               identityR : {A B : Graph.vertex G} {f : Chain G A B} → (f ・ id A) ≡ f
-               identityR {a} {_} {id a} = refl
-               identityR {a} {b} {next x f} = cong ( λ k → next x k ) ( identityR {_} {_} {f} )
-               o-resp-≈  : {A B C : Graph.vertex G} {f g : Chain G A B} {h i : Chain G B C} →
-                            f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
-               o-resp-≈  refl refl = refl
-               associative : {a b c d : Graph.vertex G} (f : Chain G c d) (g : Chain G b c) (h : Chain G a b) →
-                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
-               associative (id a) g h = refl
-               associative (next x f) g h = cong ( λ k → next x k ) ( associative f g h )
-
-
-
-data  TwoObject   : Set  where
-   t0 : TwoObject
-   t1 : TwoObject
-
----
----  two objects category  ( for limit to equalizer proof )
----
----          f
----       -----→
----     0         1
----       -----→
----          g
---
---     missing arrows are constrainted by TwoHom data
-
-data TwoHom  : TwoObject   → TwoObject  → Set  where
-   id-t0 :    TwoHom t0 t0
-   id-t1 :    TwoHom t1 t1
-   arrow-f :  TwoHom t0 t1
-   arrow-g :  TwoHom t0 t1
-
-TwoCat' : Category  Level.zero Level.zero Level.zero
-TwoCat'  = GraphtoCat ( record { vertex = TwoObject ; edge = TwoHom } )
-   where open graphtocat
-
-_×_ :  {a b c : TwoObject } →  TwoHom   b c  →  TwoHom   a b   →  TwoHom   a c 
-_×_ {t0} {t1} {t1}  id-t1   arrow-f  = arrow-f 
-_×_ {t0} {t1} {t1}  id-t1   arrow-g  = arrow-g 
-_×_ {t1} {t1} {t1}  id-t1   id-t1    = id-t1 
-_×_ {t0} {t0} {t1}  arrow-f id-t0    = arrow-f 
-_×_ {t0} {t0} {t1}  arrow-g id-t0    = arrow-g 
-_×_ {t0} {t0} {t0}  id-t0   id-t0    = id-t0 
-
-
-open TwoHom
-
---          f    g    h
---       d <- c <- b <- a
---
---   It can be proved without TwoHom constraints
-
-assoc-× :    {a b c d : TwoObject   }
-       {f : (TwoHom    c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
-       ( f × (g × h)) ≡ ((f × g) × h )
-assoc-×   {t0} {t0} {t0} {t0} { id-t0   }{ id-t0   }{ id-t0   } = refl
-assoc-×   {t0} {t0} {t0} {t1} { arrow-f }{ id-t0   }{ id-t0   } = refl
-assoc-×   {t0} {t0} {t0} {t1} { arrow-g }{ id-t0   }{ id-t0   } = refl
-assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-f }{ id-t0   } = refl
-assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-g }{ id-t0   } = refl
-assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-f } = refl
-assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-g } = refl
-assoc-×   {t1} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ id-t1   } = refl
-
-TwoId :   (a : TwoObject   ) →  (TwoHom    a a )
-TwoId  t0 = id-t0 
-TwoId   t1 = id-t1 
-
-open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
-
-TwoCat :  Category  Level.zero Level.zero Level.zero   
-TwoCat      = record {
-    Obj  = TwoObject ;
-    Hom = λ a b →   TwoHom a b  ;
-    _≈_ =  λ x y → x  ≡ y ;
-    Id  =  λ{a} → TwoId a ;
-    isCategory  = record {
-            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-            identityL  = λ{a b f} → identityL    {a} {b} {f} ;
-            identityR  = λ{a b f} → identityR    {a} {b} {f} ;
-            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = λ{a b c d f g h } → assoc-×      {a} {b} {c} {d} {f} {g} {h}
-       }
-   }  where
-        identityL :   {A B : TwoObject } {f : ( TwoHom    A B) } →  ((TwoId B)  × f)  ≡ f
-        identityL      {t1} {t1} { id-t1 } = refl
-        identityL      {t0} {t0} { id-t0 } = refl
-        identityL      {t0} {t1} { arrow-f } = refl
-        identityL      {t0} {t1} { arrow-g } = refl
-        identityR :   {A B : TwoObject } {f : ( TwoHom    A B) } →   ( f × TwoId A )  ≡ f
-        identityR      {t1} {t1} { id-t1  } = refl
-        identityR      {t0} {t0} { id-t0 } = refl
-        identityR      {t0} {t1} { arrow-f } = refl
-        identityR      {t0} {t1} { arrow-g } = refl
-        o-resp-≈ :   {A B C : TwoObject   } {f g :  ( TwoHom    A B)} {h i : ( TwoHom B C)} →
-            f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
-        o-resp-≈     {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
-
-
--- Category with no arrow but identity
-
-
-open import Data.Empty
-
-DiscreteCat' : (S : Set) → Category  Level.zero Level.zero Level.zero
-DiscreteCat'  S = GraphtoCat ( record { vertex = S ; edge = ( λ _ _ →  ⊥  ) } )
-   where open graphtocat 
-
-record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) 
-      : Set c₁ where
-   field
-      discrete : a ≡ b     -- if f : a → b then a ≡ b
-   dom : S
-   dom = a
-
-open DiscreteHom
-
-_*_ :  ∀ {c₁}  →  {S : Set c₁} {a b c : S} →  DiscreteHom {c₁}  b c  →  DiscreteHom {c₁}  a b   →  DiscreteHom {c₁}  a c 
-_*_ {_}  {a} {b} {c}  x y = record {discrete = trans ( discrete y) (discrete x) }
-
-DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) →  DiscreteHom {c₁}  a a
-DiscreteId a = record { discrete = refl }
-
-open  import  Relation.Binary.PropositionalEquality
-
-assoc-* :   {c₁  : Level } { S : Set c₁} {a b c d : S}
-       {f : (DiscreteHom  c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} →
-       dom ( f * (g * h)) ≡ dom ((f * g) * h )
-assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl
-
-DiscreteCat : {c₁ : Level  } →  (S : Set c₁) → Category   c₁   c₁   c₁  
-DiscreteCat   {c₁}  S = record {
-    Obj  = S ;
-    Hom = λ a b →   DiscreteHom  {c₁} {S} a b  ;
-    _o_ =  λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
-    _≈_ =  λ x y → dom x  ≡ dom y ;   -- x ≡ y does not work because refl ≡ discrete f is failed as it should be
-    Id  =  λ{a} → DiscreteId a ;
-    isCategory  = record {
-            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-            identityL  = λ{a b f} → identityL  {a} {b} {f} ;
-            identityR  = λ{a b f} → identityR  {a} {b} {f} ;
-            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = λ{a b c d f g h } → assoc-*  { c₁} {S}  {a} {b} {c} {d} {f} {g} {h}
-       }
-   }  where
-        identityL :   {a b : S} {f : ( DiscreteHom {c₁}  a b) } →  dom ((DiscreteId b)  * f)  ≡ dom f
-        identityL   {a} {b} {f} = refl
-        identityR :   {A B : S} {f : ( DiscreteHom {c₁}   A B) } →  dom ( f * DiscreteId A )  ≡ dom f
-        identityR   {a} {b} {f} = refl
-        o-resp-≈ :   {A B C : S } {f g :  ( DiscreteHom {c₁}   A B)} {h i : ( DiscreteHom B C)} →
-            dom f  ≡ dom g → dom h  ≡ dom i → dom ( h * f )  ≡ dom ( i * g )
-        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  refl refl = refl
-
-
-
-
-
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/graph.agda	Fri May 03 17:11:33 2019 +0900
@@ -0,0 +1,206 @@
+open import Category -- https://github.com/konn/category-agda
+open import Level
+
+module graph where
+
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
+
+record Graph  { v v' : Level } : Set (suc v ⊔ suc v' ) where
+  field
+    vertex : Set v
+    edge : vertex  → vertex → Set v'
+
+module graphtocat where
+
+  open import Relation.Binary.PropositionalEquality 
+
+  data Chain { v v' : Level } ( g : Graph {v} {v'} ) : ( a b : Graph.vertex g ) → Set (v ⊔ v' ) where
+       id : ( a : Graph.vertex g ) → Chain g a a
+       next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain g a b → Chain g a c
+
+  _・_ :  {v v' : Level} { G : Graph {v} {v'} } {a b c : Graph.vertex G } (f : Chain G b c ) → (g : Chain G a b) → Chain G a c
+  id _ ・ f = f
+  (next x f) ・ g = next x ( f ・ g )
+
+  GraphtoCat : {v v' : Level} (G : Graph {v} {v'} )  →  Category  v (v ⊔ v') (v ⊔ v')
+  GraphtoCat G = record {
+            Obj  = Graph.vertex G ;
+            Hom = λ a b →  Chain G a b ;
+            _o_ =  λ{a} {b} {c} x y → x ・ y ;
+            _≈_ =  λ x y → x  ≡ y ;
+            Id  =  λ{a} → id a ;
+            isCategory  = record {
+                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+                    identityL  = identityL; 
+                    identityR  = identityR ; 
+                    o-resp-≈  = o-resp-≈  ; 
+                    associative  = λ{a b c d f g h } → associative  f g h
+               }
+           }  where
+               open Chain
+               obj = Graph.vertex G
+               hom = Graph.edge G
+
+               identityL : {A B : Graph.vertex G} {f : Chain G A B} → (id B ・ f) ≡ f
+               identityL = refl
+               identityR : {A B : Graph.vertex G} {f : Chain G A B} → (f ・ id A) ≡ f
+               identityR {a} {_} {id a} = refl
+               identityR {a} {b} {next x f} = cong ( λ k → next x k ) ( identityR {_} {_} {f} )
+               o-resp-≈  : {A B C : Graph.vertex G} {f g : Chain G A B} {h i : Chain G B C} →
+                            f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
+               o-resp-≈  refl refl = refl
+               associative : {a b c d : Graph.vertex G} (f : Chain G c d) (g : Chain G b c) (h : Chain G a b) →
+                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
+               associative (id a) g h = refl
+               associative (next x f) g h = cong ( λ k → next x k ) ( associative f g h )
+
+
+
+data  TwoObject   : Set  where
+   t0 : TwoObject
+   t1 : TwoObject
+
+---
+---  two objects category  ( for limit to equalizer proof )
+---
+---          f
+---       -----→
+---     0         1
+---       -----→
+---          g
+--
+--     missing arrows are constrainted by TwoHom data
+
+data TwoHom  : TwoObject   → TwoObject  → Set  where
+   id-t0 :    TwoHom t0 t0
+   id-t1 :    TwoHom t1 t1
+   arrow-f :  TwoHom t0 t1
+   arrow-g :  TwoHom t0 t1
+
+TwoCat' : Category  Level.zero Level.zero Level.zero
+TwoCat'  = GraphtoCat ( record { vertex = TwoObject ; edge = TwoHom } )
+   where open graphtocat
+
+_×_ :  {a b c : TwoObject } →  TwoHom   b c  →  TwoHom   a b   →  TwoHom   a c 
+_×_ {t0} {t1} {t1}  id-t1   arrow-f  = arrow-f 
+_×_ {t0} {t1} {t1}  id-t1   arrow-g  = arrow-g 
+_×_ {t1} {t1} {t1}  id-t1   id-t1    = id-t1 
+_×_ {t0} {t0} {t1}  arrow-f id-t0    = arrow-f 
+_×_ {t0} {t0} {t1}  arrow-g id-t0    = arrow-g 
+_×_ {t0} {t0} {t0}  id-t0   id-t0    = id-t0 
+
+
+open TwoHom
+
+--          f    g    h
+--       d <- c <- b <- a
+--
+--   It can be proved without TwoHom constraints
+
+assoc-× :    {a b c d : TwoObject   }
+       {f : (TwoHom    c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
+       ( f × (g × h)) ≡ ((f × g) × h )
+assoc-×   {t0} {t0} {t0} {t0} { id-t0   }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t0} {t1} { arrow-f }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t0} {t1} { arrow-g }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-f }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-g }{ id-t0   } = refl
+assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-f } = refl
+assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-g } = refl
+assoc-×   {t1} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ id-t1   } = refl
+
+TwoId :   (a : TwoObject   ) →  (TwoHom    a a )
+TwoId  t0 = id-t0 
+TwoId   t1 = id-t1 
+
+open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
+
+TwoCat :  Category  Level.zero Level.zero Level.zero   
+TwoCat      = record {
+    Obj  = TwoObject ;
+    Hom = λ a b →   TwoHom a b  ;
+    _≈_ =  λ x y → x  ≡ y ;
+    Id  =  λ{a} → TwoId a ;
+    isCategory  = record {
+            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+            identityL  = λ{a b f} → identityL    {a} {b} {f} ;
+            identityR  = λ{a b f} → identityR    {a} {b} {f} ;
+            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
+            associative  = λ{a b c d f g h } → assoc-×      {a} {b} {c} {d} {f} {g} {h}
+       }
+   }  where
+        identityL :   {A B : TwoObject } {f : ( TwoHom    A B) } →  ((TwoId B)  × f)  ≡ f
+        identityL      {t1} {t1} { id-t1 } = refl
+        identityL      {t0} {t0} { id-t0 } = refl
+        identityL      {t0} {t1} { arrow-f } = refl
+        identityL      {t0} {t1} { arrow-g } = refl
+        identityR :   {A B : TwoObject } {f : ( TwoHom    A B) } →   ( f × TwoId A )  ≡ f
+        identityR      {t1} {t1} { id-t1  } = refl
+        identityR      {t0} {t0} { id-t0 } = refl
+        identityR      {t0} {t1} { arrow-f } = refl
+        identityR      {t0} {t1} { arrow-g } = refl
+        o-resp-≈ :   {A B C : TwoObject   } {f g :  ( TwoHom    A B)} {h i : ( TwoHom B C)} →
+            f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
+        o-resp-≈     {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
+
+
+-- Category with no arrow but identity
+
+
+open import Data.Empty
+
+DiscreteCat' : (S : Set) → Category  Level.zero Level.zero Level.zero
+DiscreteCat'  S = GraphtoCat ( record { vertex = S ; edge = ( λ _ _ →  ⊥  ) } )
+   where open graphtocat 
+
+record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) 
+      : Set c₁ where
+   field
+      discrete : a ≡ b     -- if f : a → b then a ≡ b
+   dom : S
+   dom = a
+
+open DiscreteHom
+
+_*_ :  ∀ {c₁}  →  {S : Set c₁} {a b c : S} →  DiscreteHom {c₁}  b c  →  DiscreteHom {c₁}  a b   →  DiscreteHom {c₁}  a c 
+_*_ {_}  {a} {b} {c}  x y = record {discrete = trans ( discrete y) (discrete x) }
+
+DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) →  DiscreteHom {c₁}  a a
+DiscreteId a = record { discrete = refl }
+
+open  import  Relation.Binary.PropositionalEquality
+
+assoc-* :   {c₁  : Level } { S : Set c₁} {a b c d : S}
+       {f : (DiscreteHom  c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} →
+       dom ( f * (g * h)) ≡ dom ((f * g) * h )
+assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl
+
+DiscreteCat : {c₁ : Level  } →  (S : Set c₁) → Category   c₁   c₁   c₁  
+DiscreteCat   {c₁}  S = record {
+    Obj  = S ;
+    Hom = λ a b →   DiscreteHom  {c₁} {S} a b  ;
+    _o_ =  λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
+    _≈_ =  λ x y → dom x  ≡ dom y ;   -- x ≡ y does not work because refl ≡ discrete f is failed as it should be
+    Id  =  λ{a} → DiscreteId a ;
+    isCategory  = record {
+            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+            identityL  = λ{a b f} → identityL  {a} {b} {f} ;
+            identityR  = λ{a b f} → identityR  {a} {b} {f} ;
+            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
+            associative  = λ{a b c d f g h } → assoc-*  { c₁} {S}  {a} {b} {c} {d} {f} {g} {h}
+       }
+   }  where
+        identityL :   {a b : S} {f : ( DiscreteHom {c₁}  a b) } →  dom ((DiscreteId b)  * f)  ≡ dom f
+        identityL   {a} {b} {f} = refl
+        identityR :   {A B : S} {f : ( DiscreteHom {c₁}   A B) } →  dom ( f * DiscreteId A )  ≡ dom f
+        identityR   {a} {b} {f} = refl
+        o-resp-≈ :   {A B C : S } {f g :  ( DiscreteHom {c₁}   A B)} {h i : ( DiscreteHom B C)} →
+            dom f  ≡ dom g → dom h  ≡ dom i → dom ( h * f )  ≡ dom ( i * g )
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  refl refl = refl
+
+
+
+
+
+
--- a/limit-to.agda	Thu May 02 11:54:09 2019 +0900
+++ b/limit-to.agda	Fri May 03 17:11:33 2019 +0900
@@ -9,7 +9,7 @@
 open  import  Relation.Binary.PropositionalEquality hiding ([_])
 
 
-open import discrete
+open import graph
 
 
 ---  Equalizer  from Limit ( 2→A IdnexFunctor Γ and  IndexNat :  K →　Γ)
@@ -157,7 +157,7 @@
 
 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} → (f g : Hom A a b)  (lim : Limit TwoCat A (IndexFunctor A a b f g) ) →
          Hom A (a0 lim) a
-equlimit A {a} {b} f g lim = TMap (Limit.t0 lim) discrete.t0
+equlimit A {a} {b} f g lim = TMap (Limit.t0 lim) graph.t0
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
         →  {a b : Obj A}  (f g : Hom A  a b )
@@ -183,11 +183,11 @@
          fe=ge0 = let open  ≈-Reasoning A in  begin
                     f o (equlimit A f g lim )
                 ≈⟨⟩
-                    FMap  Γ arrow-f o TMap (Limit.t0 lim) discrete.t0
-                ≈⟨  IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-f} ⟩ 
-                    TMap (Limit.t0 lim) discrete.t1 o FMap (K (TwoCat   ) A (a0 lim)) id-t0
-                ≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-g} ⟩ 
-                    FMap  Γ arrow-g o TMap (Limit.t0 lim) discrete.t0
+                    FMap  Γ arrow-f o TMap (Limit.t0 lim) graph.t0
+                ≈⟨  IsNTrans.commute ( isNTrans (Limit.t0 lim)) {graph.t0} {graph.t1} {arrow-f} ⟩ 
+                    TMap (Limit.t0 lim) graph.t1 o FMap (K (TwoCat   ) A (a0 lim)) id-t0
+                ≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {graph.t0} {graph.t1} {arrow-g} ⟩ 
+                    FMap  Γ arrow-g o TMap (Limit.t0 lim) graph.t0
                 ≈⟨⟩
                     g o (equlimit A f g lim )
                 ∎
@@ -197,9 +197,9 @@
          ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
                     e o k h fh=gh
                 ≈⟨⟩
-                    TMap (Limit.t0 lim) discrete.t0  o k h fh=gh
-                ≈⟨ t0f=t (isLimit lim) {d} {inat d h fh=gh } {discrete.t0}  ⟩
-                    TMap (inat d h fh=gh) discrete.t0
+                    TMap (Limit.t0 lim) graph.t0  o k h fh=gh
+                ≈⟨ t0f=t (isLimit lim) {d} {inat d h fh=gh } {graph.t0}  ⟩
+                    TMap (inat d h fh=gh) graph.t0
                 ≈⟨⟩
                     h
                 ∎
@@ -207,13 +207,13 @@
                        ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ]) → A [ A [ e o k' ] ≈ h ] →
                        A [ A [ TMap (Limit.t0 lim) i o k' ] ≈ TMap (inat d h fh=gh) i ]
          uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
-                    TMap (Limit.t0 lim) discrete.t0 o k'
+                    TMap (Limit.t0 lim) graph.t0 o k'
                 ≈⟨⟩
                     e o k'
                 ≈⟨ ek'=h ⟩
                     h
                 ≈⟨⟩
-                    TMap (inat d h fh=gh) discrete.t0
+                    TMap (inat d h fh=gh) graph.t0
                 ∎
          uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
                     TMap (Limit.t0 lim) t1 o k'
@@ -222,7 +222,7 @@
                 ≈⟨⟩
                     ( TMap (Limit.t0 lim) t1  o  FMap (K I A c) arrow-f ) o k'
                 ≈↑⟨ car ( nat1 (Limit.t0 lim) arrow-f ) ⟩
-                    ( FMap Γ  arrow-f  o TMap (Limit.t0 lim) discrete.t0 ) o k'
+                    ( FMap Γ  arrow-f  o TMap (Limit.t0 lim) graph.t0 ) o k'
                 ≈⟨⟩
                    (f o e ) o k'
                 ≈↑⟨ assoc ⟩