Mercurial > hg > Members > kono > Proof > category

changeset 901:9652159bda4b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CCC to Graph forgetful functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 Apr 2020 11:24:32 +0900
parents eaf90711a6fd
children 6633314ba902
files CCCGraph.agda
diffstat 1 files changed, 5 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Wed Apr 29 04:07:44 2020 +0900
+++ b/CCCGraph.agda	Wed Apr 29 11:24:32 2020 +0900
@@ -398,26 +398,16 @@
 fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b )
 fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) ; econg = IsFunctor.≈-cong (Functor.isFunctor (cmap f))  }
 
-UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) →  {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g  )
-    → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} {ℓ} )
-FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡  ) a = fobj a
-FMap (UX ≈-to-≡)  f =  fmap f
-isFunctor (UX {c₁} {c₂} {ℓ}  ≈-to-≡)  = isf where
-  -- if we don't need ≈-cong ( i.e.   f ≈ g → UX f =m= UX g ), all lemmas are not necessary
-  open import HomReasoning
-  isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}) fobj fmap
+UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} {ℓ} )
+FObj UX a = fobj a
+FMap UX f =  fmap f
+isFunctor UX  = isf where
+  isf : IsFunctor Cart Grph 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} 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