# HG changeset patch # User Shinji KONO <kono@ie.u-ryukyu.ac.jp> # Date 1377657677 -32400 # Node ID 2d983d843e29f7eac49c15bf1b27d63ece4cccfe # Parent f017d892d8c3e85e66042415572aea65c1e1295d no yellow on co-Contravariant Functor diff -r f017d892d8c3 -r 2d983d843e29 yoneda.agda --- a/yoneda.agda Wed Aug 28 10:20:04 2013 +0900 +++ b/yoneda.agda Wed Aug 28 11:41:17 2013 +0900 @@ -12,18 +12,23 @@ -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) open Functor -CF : (a : Obj A) → Functor (Category.op A) Sets +CF : (a : Obj A) → Functor A Sets CF a = record { FObj = λ b → Hom A a b - ; FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → {!!} + ; FMap = λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) → A [ f o g ] ; isFunctor = record { - identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) - ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) + identity = identity + ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g ; ≈-cong = cong1 } } where - cong1 : {b c : Obj A } { f g : Hom A b c} → A [ f ≈ g ] → Sets [ {!!} ≈ {!!} ] - cong1 eq = _≡_.refl + identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ] + identity = let open ≈-Reasoning A in {!!} + distr1 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → + Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ] + distr1 a b c f g = {!!} + cong1 : {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ] + cong1 eq = {!!}