# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556422654 -32400
# Node ID 17716299087918fdeceb7503148017e1aaf3a109
# Parent  4e48b331020ab733b10e333b28427c94aca3a7cf
...

diff -r 4e48b331020a -r 177162990879 CCCGraph.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CCCGraph.agda	Sun Apr 28 12:37:34 2019 +0900
@@ -0,0 +1,237 @@
+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 {
+         １  = One
+       ; ○ = λ _ → λ _ → OneObj
+       ; _∧_ = _∧_
+       ; <_,_> = <,>
+       ; π = π
+       ; π' = π'
+       ; _<=_ = _<=_
+       ; _* = _*
+       ; ε = ε
+       ; isCCC = isCCC
+  } where
+         １ : Obj Sets 
+         １ = One 
+         ○ : (a : Obj Sets ) → Hom Sets a １
+         ○ 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 １ ○ _∧_ <,> π π' _<=_ _* ε
+         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 １} → 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 ) : 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 )
+
+   record SM {v : Level} : Set (suc v)  where
+      field
+        graph : Graph  {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 ) 
+
+---   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 : {A B : CCCObj {c₁} {c₂} {ℓ} } → CCC (cat A) → CCC (cat B)
+---   
+---   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_ = {!!}
+---     ; _≈_ = {!!}
+---     ; Id  = {!!}
+---     ; isCategory = record {
+---          identityL = {!!}
+---        ; identityR = {!!}
+---        ; o-resp-≈ = {!!}
+---        ; associative = {!!}
+---      }}
+---   
+---   open import discrete
+---   open Graph
+---   
+---   record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where
+---      vmap : vertex x → vertex y
+---      emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
+---   
+---   Grp : {v : Level} → Category (suc v) v v
+---   Grp {v} = record {
+---       Obj = Graph {v} 
+---     ; Hom = {!!}
+---     ; _o_ = {!!}
+---     ; _≈_ = {!!}
+---     ; Id  = {!!}
+---     ; isCategory = record {
+---          identityL = {!!}
+---        ; identityR = {!!}
+---        ; o-resp-≈ = {!!}
+---        ; associative = {!!}
+---      }}
+---   
+---   UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁})
+---   UX = {!!}
+---   
+---   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 } )
+---   
+---   
+---   
+---   
diff -r 4e48b331020a -r 177162990879 CCChom.agda
--- a/CCChom.agda	Sat Apr 27 12:58:12 2019 +0900
+++ b/CCChom.agda	Sun Apr 28 12:37:34 2019 +0900
@@ -376,8 +376,6 @@
              ∎ where open ≈-Reasoning A
 
 
-
-
 open CCChom
 open IsCCChom
 open IsoS
@@ -524,160 +522,3 @@
                *-cong  : {a b c : Obj A} {f f' : Hom A (a ∧ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
                *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
 
-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 {
-         １  = One'
-       ; ○ = λ _ → λ _ → OneObj'
-       ; _∧_ = _∧_
-       ; <_,_> = <,>
-       ; π = π
-       ; π' = π'
-       ; _<=_ = _<=_
-       ; _* = _*
-       ; ε = ε
-       ; isCCC = isCCC
-  } where
-         １ : Obj Sets 
-         １ = One' 
-         ○ : (a : Obj Sets ) → Hom Sets a １
-         ○ 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 １ ○ _∧_ <,> π π' _<=_ _* ε
-         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 １} → 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 ) : 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 )
-
-   record SM  : Set (suc Level.zero)  where
-      field
-        graph : Graph 
-        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 ) 
-
diff -r 4e48b331020a -r 177162990879 discrete.agda
--- a/discrete.agda	Sat Apr 27 12:58:12 2019 +0900
+++ b/discrete.agda	Sun Apr 28 12:37:34 2019 +0900
@@ -6,27 +6,27 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
 
-record Graph : Set (Level.suc Level.zero ) where
+record Graph  { v : Level } : Set (suc v) where
   field
-    vertex : Set
-    edge : vertex  → vertex → Set
+    vertex : Set v
+    edge : vertex  → vertex → Set v
 
 module graphtocat where
 
   open import Relation.Binary.PropositionalEquality 
 
-  data Chain { g : Graph } : ( a b : Graph.vertex g ) → Set where
-       id : ( a : Graph.vertex g ) → Chain a a
-       next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain {g} a b → Chain  a c
+  data Chain { v : Level } ( g : Graph {v} ) : ( a b : Graph.vertex g ) → Set 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
 
-  _・_ : { G : Graph} {a b c : Graph.vertex G } (f : Chain {G} b c ) → (g : Chain {G} a b) → Chain {G} a c
+  _・_ :  {v : Level} { G : Graph {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 : (G : Graph )  →  Category  Level.zero Level.zero Level.zero   
+  GraphtoCat : {v : Level} (G : Graph {v} )  →  Category  v v v
   GraphtoCat G = record {
             Obj  = Graph.vertex G ;
-            Hom = λ a b →  Chain {G} a b ;
+            Hom = λ a b →  Chain G a b ;
             _o_ =  λ{a} {b} {c} x y → x ・ y ;
             _≈_ =  λ x y → x  ≡ y ;
             Id  =  λ{a} → id a ;
@@ -42,15 +42,15 @@
                obj = Graph.vertex G
                hom = Graph.edge G
 
-               identityL : {A B : Graph.vertex G} {f : Chain A B} → (id B ・ f) ≡ f
+               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 A B} → (f ・ id A) ≡ f
+               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 A B} {h i : Chain B C} →
+               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 c d) (g : Chain b c) (h : Chain a b) →
+               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 )