Mercurial > hg > Members > kono > Proof > category
changeset 936:d13e0981e667
η on Graph to CCC
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 15 May 2020 20:10:09 +0900 |
| parents | 92f8f57467e3 |
| children | 2385fdd6818b |
| files | CCCGraph.agda |
| diffstat | 1 files changed, 9 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph.agda Fri May 15 17:59:15 2020 +0900 +++ b/CCCGraph.agda Fri May 15 20:10:09 2020 +0900 @@ -416,7 +416,7 @@ open forgetful open ccc-from-graph -- η : Hom Grph a (FObj UX (F a)) - -- f : edge g x y -----------------------------------> g21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph + -- f : edge g x y -----------------------------------> m21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph -- Graph g x ----------------------> y : vertex g ↑ -- arrow f : Hom (PL g) (atom x) (atom y) | -- PL g atom x ------------------> atom y : Obj (PL g) | UX : Functor Sets Graph @@ -430,7 +430,14 @@ F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) F g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a)) - η a = record { vmap = λ y → {!!} y ; emap = λ f → {!!} } where + η a = record { vmap = λ y → vm y ; emap = λ f → em f } where + fo : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} + fo = forgetful.fobj {c₁} {c₂} (F a) + vm : (y : vertex a ) → vertex (g21 fo) + vm y = vmap (m21 fo) (ccc-from-graph.fobj a (atom y)) + em : { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y) + em {x} {y} f = emap (m21 fo) (ccc-from-graph.fmap a (iv (arrow f) (id _))) + -- k : ( y : vertex a) → Set (c₁ ⊔ c₂) -- k y = ( e : vertex a ) → graphtocat.Chain a e y -- mm : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}