Mercurial > hg > Members > kono > Proof > category
changeset 928:c1222aa20244
level loop on ccc-graph-univ
locally small mapping will be necessary
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 May 2020 20:27:36 +0900 |
| parents | 2c5ae3015a05 |
| children | 1e8ed7dedc03 |
| files | CCCGraph.agda |
| diffstat | 1 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/CCCGraph.agda Sun May 10 16:36:42 2020 +0900 +++ b/CCCGraph.agda Sun May 10 20:27:36 2020 +0900 @@ -367,8 +367,8 @@ ccc-graph-univ : {c₁ c₂ : Level } → UniversalMapping (Grph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}) (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (forgetful.UX {c₁} {c₂} ) ccc-graph-univ {c₁} {c₂} = record { - F = λ g → csc {!!} ; - η = λ a → record { vmap = λ y → cobj {!!} {!!}; emap = λ f x y → next f (x y) } ; + F = λ g → csc {!!} ; -- g + η = λ a → record { vmap = λ y → {!!} ; emap = λ f x y → next f (x y) } ; -- graphtocat.Chain a ? ? _* = solution ; isUniversalMapping = record { universalMapping = {!!} ; @@ -398,6 +398,6 @@ 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 {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)})} {c : Obj (Cart )} → Hom Grph g (FObj UX c) → Hom (Cart ) {!!} {!!} - solution {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} } + solution {g} {c} f = ? -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }