Mercurial > hg > Members > kono > Proof > category

changeset 941:d26f21112e1c

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 10:32:22 +0900
parents 6847eba130bd
children 5084433e0726
files CCCGraph.agda
diffstat 1 files changed, 7 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sun May 17 09:24:40 2020 +0900
+++ b/CCCGraph.agda	Sun May 17 10:32:22 2020 +0900
@@ -382,14 +382,7 @@
   isFunctor UX  = isf where
     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 ) mf=f mf=f m  where
-         fuga : vmap (m12 (fobj a)) ((vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f))) ≡ vmap (m12 (fobj a)) f
-         fuga = eq-vertex1 (fobj a) tt
-         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) _)
+    eff a f = {!!}
     IsFunctor.identity isf {a} {b} {f} = begin
          fmap (id1 Cart a) 
        ≈⟨⟩
@@ -403,7 +396,13 @@
        ∎ where open ≈-Reasoning Grph 
     IsFunctor.distr isf {a} {b} {c} {f} {g} = begin
          fmap ( Cart [ g o f ] )
+       ≈⟨⟩
+         record { vmap = λ e →  vmap (m21 (fobj c)) (FObj (cmap (Cart [ g o f ] )) (vmap (m12 (fobj a)) e)) ;
+                  emap = λ e →  emap (m21 (fobj c)) (FMap (cmap (Cart [ g o f ] )) (emap (m12 (fobj a)) e)) } 
        ≈⟨ {!!} ⟩
+         record { vmap = λ e →  vmap (m21 (fobj c)) (FObj (cmap g) (vmap (m12 (fobj b)) (vmap (fmap f) e)));
+                  emap = λ e →  emap (m21 (fobj c)) (FMap (cmap g) (emap (m12 (fobj b)) (emap (fmap f) e))) } 
+       ≈⟨⟩
          Grph [ fmap g o fmap f ]
        ∎ where open ≈-Reasoning Grph 
     IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 (