Mercurial > hg > Members > kono > Proof > category

changeset 900:eaf90711a6fd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Forgetful functor from CCC to Graph done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 Apr 2020 04:07:44 +0900
parents e20853d2c6b0
children 9652159bda4b
files CCCGraph.agda
diffstat 1 files changed, 11 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Wed Apr 29 03:01:05 2020 +0900
+++ b/CCCGraph.agda	Wed Apr 29 04:07:44 2020 +0900
@@ -408,18 +408,20 @@
   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} 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 = {!!}
+  IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 (
+               ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
+          )))) (f=g e) where
+    -- ... | 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
-    --  lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
-    --  lemma4 (refl eqv) = refl 
-    --  lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
-    --  lemma refl (refl eqv) = mrefl {!!} -- (econg (fmap f ) ? ) -- ( ≈-to-≡ (cat b) eqv )
+    lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
+    lemma4 (refl eqv) = refl 
+    lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
+    lemma refl (refl eqv) = mrefl eqv