Mercurial > hg > Members > kono > Proof > category

changeset 179:f017d892d8c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Aug 2013 10:20:04 +0900
parents 6626a7cd9129
children 2d983d843e29
files yoneda.agda
diffstat 1 files changed, 9 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Tue Aug 27 23:35:05 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 10:20:04 2013 +0900
@@ -5,23 +5,25 @@
 
 open import HomReasoning
 open import cat-utility
-open import Category.Cat
+open import Relation.Binary.Core
+open import Relation.Binary
+
 
 -- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
+open Functor
 
-CF : (a : Obj A) → Functor (op A) Sets
+CF : (a : Obj A) → Functor (Category.op A) Sets
 CF a = record {
         FObj = λ b → Hom A a b
-        ; FMap = {b c : Obj A } λ (f : Hom A b c) → (Hom A c a) → (Hom A b a)
+        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A c b ) → {!!} 
         ; isFunctor = record {
              identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
              ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
              ; ≈-cong = cong1
         } 
     } where
-        cong1 : {ℓ′ : Level} → {b c : Set ℓ′} { f g : Hom (Sets {ℓ′}) b c} → 
-                   Sets [ f ≈ g ] → Sets [ f ≈  g ]
-        cong1 _≡_.refl = _≡_.refl
+        cong1 : {b c : Obj A } { f g : Hom  A b c} → A [ f ≈ g ] →   Sets [ {!!} ≈ {!!} ] 
+        cong1 eq = _≡_.refl
 
-open Functor
 
+