Mercurial > hg > Members > kono > Proof > category

changeset 178:6626a7cd9129

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Yoneda Functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 27 Aug 2013 23:35:05 +0900
parents 63f6157a6a19
children f017d892d8c3
files category.pdf free-monoid.agda yoneda.agda
diffstat 3 files changed, 33 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
Binary file category.pdf has changed
--- a/free-monoid.agda	Sun Aug 25 11:10:35 2013 +0900
+++ b/free-monoid.agda	Tue Aug 27 23:35:05 2013 +0900
@@ -13,6 +13,7 @@
 open import cat-utility
 open import Relation.Binary.Core
 open import  Relation.Binary.PropositionalEquality
+open import universal-mapping 
 
 -- from https://github.com/danr/Agda-projects/blob/master/Category-Theory/FreeMonoid.agda
 
@@ -268,8 +269,11 @@
                                (morph g) ( x :: []  )
                              ∎   
 
- 
-open import universal-mapping 
+open NTrans
+--   fm-ε b = Φ
+fm-ε :  NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor
+fm-ε =  nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping 
+--  TMap fm-ε
 
 adjoint  = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping 
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/yoneda.agda	Tue Aug 27 23:35:05 2013 +0900
@@ -0,0 +1,27 @@
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+open import Category.Sets
+module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+
+open import HomReasoning
+open import cat-utility
+open import Category.Cat
+
+-- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
+
+CF : (a : Obj A) → Functor (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)
+        ; 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
+
+open Functor
+