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 -------- -- -- Graph to positive logic -- open import graph module ccc-from-graph {c₁ c₂ ℓ : Level} (G : Graph {c₁} {c₂} {ℓ}) where open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Binary.Core open Graph data Objs : Set (c₁ ⊔ 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 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 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v data Arrows where id : ( a : Objs ) → Arrows a a --- case i ○ : ( a : Objs ) → Arrows a ⊤ --- case i <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c id a ・ g = g ○ a ・ g = ○ _ < f , g > ・ h = < f ・ h , g ・ h > iv f g ・ h = iv f ( g ・ h ) identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f identityR {a} {a} {id a} = refl identityR {a} {⊤} {○ a} = refl identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f identityL = refl associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) → (f ・ (g ・ h)) ≡ ((f ・ g) ・ h) associative (id a) g h = refl associative (○ a) g h = refl associative < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (associative f g h) (associative f₁ g h) associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h ) -- positive intutionistic calculus PL : Category (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂) PL = record { Obj = Objs; Hom = λ a b → Arrows 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 = λ {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 } → associative f g h } } where o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} → f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g) o-resp-≈ refl refl = refl -------- -- -- Functor from Positive Logic to Sets -- -- open import Category.Sets -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality 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) fobj : ( a : Objs ) → Set (c₁ ⊔ c₂ ⊔ ℓ) fobj (atom x) = ( y : vertex G ) → C y x fobj ⊤ = One fobj (a ∧ b) = ( fobj a /\ fobj b) fobj (a <= b) = fobj b → fobj a 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 π ( x , y ) = x amap π' ( x , y ) = y amap ε (f , x ) = f x amap (f *) x = λ y → fmap f ( x , y ) fmap (id a) x = x fmap (○ a) x = OneObj fmap < f , g > x = ( fmap f x , fmap g x ) fmap (iv x f) a = amap x ( fmap f a ) -- 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 : 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) distr {a} {a₁} {a₁} {f} {id a₁} z = refl distr {a} {a₁} {⊤} {f} {○ a₁} z = refl distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k → j , k ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z) distr {a} {b} {c} {f} {iv {_} {_} {d} 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 d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z ) adistr eq x = cong ( λ k → amap x k ) eq isf : IsFunctor PL 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 ) open import subcat CSC = FCat PL (Sets {c₁ ⊔ c₂ ⊔ ℓ}) CS cc1 : CCC CSC -- SCS is CCC cc1 = record { １ = ⊤ ; ○ = λ a x → OneObj ; _∧_ = λ x y → x ∧ y ; <_,_> = λ f g x → ( f x , g x ) ; π = proj₁ ; π' = proj₂ ; _<=_ = λ b a → b <= a ; _* = λ f x y → f ( x , y ) ; ε = λ x → ( proj₁ x) (proj₂ x) ; isCCC = record { e2 = λ {a} {f} → extensionality Sets ( λ x → e20 {a} {f} x ) ; e3a = refl ; e3b = refl ; e3c = refl ; π-cong = π-cong ; e4a = refl ; e4b = refl ; *-cong = *-cong } } where e20 : {a : Obj CSC} {f : Hom CSC a ⊤} (x : fobj a ) → f x ≡ OneObj e20 {a} {f} x with f x e20 x | OneObj = 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 [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ] π-cong refl refl = refl *-cong : {a b c : Obj CSC } {f f' : Hom CSC (a ∧ b) c} → Sets [ f ≈ f' ] → Sets [ (λ x y → f (x , y)) ≈ (λ x y → f' (x , y)) ] *-cong refl = refl ------------------------------------------------------ -- Cart Category of CCC and CCC preserving Functor ------------------------------------------------------ --- --- SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap --- --- CCC ( SC (CS G)) Sets have to be proved --- SM can be eliminated if we have --- sobj (a : vertex g ) → {a} a set have only a --- smap (a b : vertex g ) → {a} → {b} 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 : CCC (cat A) → CCC (cat B) open import Category.Cat 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₂} {ℓ} ; 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 ; Id = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x } ; isCategory = record { isEquivalence = λ {A} {B} → record { refl = λ {f} → let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} ; sym = λ {f} {g} → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h} } ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_} ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f} ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i} → IsCategory.o-resp-≈ ( Category.isCategory CAT) {cat x}{cat y}{cat z} {cmap f} {cmap g} {cmap h} {cmap i} ; 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} }} ------------------------------------------------------ -- Grph Category of Graph and Graph mapping ------------------------------------------------------ open import graph open Graph 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) econg : {a b : vertex x} → { f g : edge x a b } → Graph._≅_ x f g → Graph._≅_ y (emap f) (emap g) open GMap -- 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 mrefl : {g : edge C A B} → (eqv : Graph._≅_ C f g ) → [ C ] f == g _=m=_ : ∀ {c₁ c₂ ℓ} {C D : Graph {c₁} {c₂} {ℓ}} → (F G : GMap C D) → Set (suc (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 _&_ : {v v' ℓ : Level} {x y z : Graph {v} {v'} {ℓ}} ( 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 ) ; econg = λ eq → econg f ( econg g eq) } erefl : {v v' ℓ : Level} (C : Graph {v} {v'} {ℓ}) → { x y : vertex C } → {f : edge C x y } → Graph._≅_ C f f erefl C = IsEquivalence.refl (Graph.isEq C) Grph : {v v' ℓ : Level} → Category (suc (v ⊔ v' ⊔ ℓ )) (suc (v ⊔ v' ⊔ ℓ)) (suc ( v ⊔ v' ⊔ ℓ)) Grph {v} {v'} {ℓ} = record { Obj = Graph {v} {v'} {ℓ} ; Hom = GMap {v} {v'} ; _o_ = _&_ ; _≈_ = _=m=_ ; Id = record { vmap = λ y → y ; emap = λ f → f ; econg = λ eq → eq } ; isCategory = record { isEquivalence = λ {A} {B} → ise ; identityL = λ {a} {b} {f} e → mrefl ( erefl b ) ; identityR = λ {a} {b} {f} e → mrefl ( erefl b) ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} f=g h=i → m--resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i ; associative = λ {a} {b} {c} {d} {f} {g} {h} e → mrefl (erefl d ) }} where msym : {x y : Graph {v} {v'} {ℓ}} { 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 (IsEquivalence.sym (Graph.isEq y) Ff≈Gf) mtrans : {x y : Graph {v} {v'} {ℓ}} { 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 ( (IsEquivalence.trans (Graph.isEq y)) eqv eqv₁ ) ise : {x y : Graph {v} {v'} {ℓ}} → IsEquivalence {_} {suc v ⊔ suc v' ⊔ suc ℓ} {_} ( _=m=_ {v} {v'} {ℓ} {x} {y}) ise {x} {y} = record { refl = λ {C} f → mrefl (erefl y ) ; sym = λ {x} {y} eq → msym {_} {_} {x} {y} eq ; trans = λ {x} {y} {z} eq → mtrans {_} {_} {x} {y} {z} eq } m--resp-≈ : {A B C : Graph {v} {v'}{ℓ} } {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 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 ϕ) == π lemma ϕ ψ π (mrefl f=g ) (mrefl h=i ) = mrefl ( (IsEquivalence.trans (Graph.isEq C)) (econg h f=g ) h=i ) ------------------------------------------------------ --- CCC → Grph Forgetful functor ------------------------------------------------------ ≃-cong : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B } → { f f' : Hom B a b } → { g g' : Hom B a' b' } → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g' ≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'} (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin f' ≈↑⟨ f=f' ⟩ f ≈⟨ eqv ⟩ g ≈⟨ g=g' ⟩ g' ∎ ) fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} ) → Obj (Grph {c₁} {c₂}{ℓ}) fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) ; _≅_ = Category._≈_ (cat a) ; isEq = IsCategory.isEquivalence (Category.isCategory (cat a)) } fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b ) fmap f = record { vmap = FObj (cmap f) ; emap = FMap (cmap f) ; econg = IsFunctor.≈-cong (Functor.isFunctor (cmap f)) } UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) → {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g ) → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} {ℓ} ) FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡ ) a = fobj a FMap (UX ≈-to-≡) f = fmap f isFunctor (UX {c₁} {c₂} {ℓ} ≈-to-≡) = isf where -- if we don't need ≈-cong ( i.e. f ≈ g → UX f =m= UX g ), all lemmas are not necessary open import HomReasoning isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap IsFunctor.identity isf {a} {b} {f} e = mrefl (erefl (fobj a)) IsFunctor.distr isf {a} {b} {c} f = mrefl (erefl (fobj c)) IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 ( ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) )))) (f=g e) where -- ... | t | x | y | record { eq = ee } = lemma x y {!!} where -- lemma : ( x : Hom (cat b) (FObj (cmap f) A) (FObj (cmap f) B) ) ( y : Hom (cat b) (FObj (cmap g) A) (FObj (cmap g) B) ) → -- [ cat b ] x ~ y → [ fobj b ] x == y -- lemma x y t2 = {!!} -- lemma (extensionality Sets ( λ z → lemma4 ( -- ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) -- ))) (eq e) where lemma4 : {x y : vertex (fobj b) } → [_]_~_ (cat b) (id1 (cat b) x) (id1 (cat b) y) → x ≡ y lemma4 (refl eqv) = refl lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e lemma refl (refl eqv) = mrefl eqv open ccc-from-graph --- HX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) → {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g ) --- → Functor (Grph {c₁} {c₂}) (Cart {c₁} {c₂} {ℓ} ) --- HX = {!!}