Mercurial > hg > Members > kono > Proof > category

changeset 899:e20853d2c6b0

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 Wed, 29 Apr 2020 03:01:05 +0900
parents d1bd473b4efb
children eaf90711a6fd
files CCCGraph.agda
diffstat 1 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Tue Apr 28 16:16:16 2020 +0900
+++ b/CCCGraph.agda	Wed Apr 29 03:01:05 2020 +0900
@@ -408,8 +408,11 @@
   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} eq {x} {y} e = {!!} where --  [ fobj b ] emap (fmap f) e == emap (fmap g) e
-        lemma = econg (fmap f) {!!}
+  IsFunctor.≈-cong isf {a} {b} {f} {g} eq1 {A} {B} e with eq1 {A} {B} e | FMap (cmap f) e | FMap (cmap g) e | inspect eq1 e
+  ... | 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