Mercurial > hg > Members > kono > Proof > category

changeset 939:d918ab22419f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 17 May 2020 09:17:39 +0900
parents 24248f9249c5
children 6847eba130bd
files CCCGraph.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sat May 16 23:45:33 2020 +0900
+++ b/CCCGraph.agda	Sun May 17 09:17:39 2020 +0900
@@ -383,11 +383,11 @@
     isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap
     eff : (a : Obj Cart) (f : vertex (g21 (fobj a)) ) → edge (g21 (fobj a)) f f
     eff a f with giso→ {fobj a} {_} {_} {id1 (cat a) (vmap (m12 (fobj a)) f )} (id1 (cat a) (vmap (m12 (fobj a)) f )) 
-    ... | tt = subst₂ (λ j k → edge (g21 (fobj a)) j k ) {!!} {!!} m  where
-         fuga : ? ≡ ?
+    ... | tt = subst₂ (λ j k → edge (g21 (fobj a)) j k ) mf=f mf=f m  where
+         fuga : {!!} ≡ {!!}
          fuga = eq-vertex1 (fobj a) tt
-         hoge : vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f) ≡ f
-         hoge = eq-vertex1 (g21 (fobj a)) {!!}
+         mf=f : vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f) ≡ f
+         mf=f = eq-vertex1 (g21 (fobj a)) (giso← {!!} )
          m :  edge (g21 (fobj a)) (vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f )) (vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f ))
          m  = emap (m21 (fobj a)) (id1 (cat a) _)
     IsFunctor.identity isf {a} {b} {f} = begin
@@ -487,7 +487,7 @@
             }
        solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c
        solution  {g} {c} f = record { cmap = record {
-             FObj = λ x → cobj {g} {c} f (xtog x) ;
+             FObj = λ x → cobj {g} {c} f (xtog x ) ;
              FMap = λ {x} {y} h → c-map {g} {c} f (htop {x} {y} h )  ;
              isFunctor = {!!} } ;
              ccf = {!!} } where
@@ -495,8 +495,8 @@
                 mp = record { vmap = {!!} ; emap = {!!} }
                 mm : Hom Grph g (forgetful.fobj c)
                 mm = mp & f
-                xtog : Obj Sets → Objs g
-                xtog x = {!!}
+                xtog : (x : Obj Sets) → Objs g
+                xtog x = ccc-from-graph.atom {!!}
                 htop : {x y : Set (c₁ ⊔ c₂) } → (x → y) →  Hom (pl g) (xtog x) (xtog y)
                 htop = {!!}
                 fo : Graph  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}