Mercurial > hg > Members > kono > Proof > category

changeset 202:58ee98bbb333

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove an extensionality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 01 Sep 2013 13:26:30 +0900
parents eb935f04bf39
children 1c16d18a8d67
files cat-utility.agda free-monoid.agda monoid-monad.agda yoneda.agda
diffstat 4 files changed, 65 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sat Aug 31 12:53:35 2013 +0900
+++ b/cat-utility.agda	Sun Sep 01 13:26:30 2013 +0900
@@ -56,6 +56,10 @@
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
             field
                isAdjunction : IsAdjunction A B U F η ε
+            U-functor =  U
+            F-functor =  F
+            Eta = η
+            Epsiron = ε
 
 
         record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
--- a/free-monoid.agda	Sat Aug 31 12:53:35 2013 +0900
+++ b/free-monoid.agda	Sun Sep 01 13:26:30 2013 +0900
@@ -161,6 +161,7 @@
 
 open UniversalMapping
 
+--   [a,b,c] → f(a) ∙ f(b) ∙ f(c)
 Φ :  {a : Obj A } {b : Obj B} { f : Hom A a (FObj U b) } →  List a -> Carrier b
 Φ {a} {b} {f} [] = ε b
 Φ {a} {b} {f} ( x :: xs ) = _∙_ b  ( f x ) (Φ {a} {b} {f} xs )
@@ -275,8 +276,16 @@
 fm-ε =  nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping 
 --  TMap fm-ε
 
-adjoint  = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping 
+open Adjunction
 
+-- A = Sets {c}
+-- B = Monoids  
+-- U   underline funcotr
+-- F   generator = x :: []
+-- Eta          x :: []
+-- Epsiron      morph = Φ
+
+adj = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping 
 
  
 
--- a/monoid-monad.agda	Sat Aug 31 12:53:35 2013 +0900
+++ b/monoid-monad.agda	Sun Sep 01 13:26:30 2013 +0900
@@ -183,4 +183,9 @@
 
 open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad}
 
-
+-- nat-ε   TMap = λ a₁ → record { KMap = λ x → x }
+-- nat-η   TMap = λ a₁ → _,_ (ε,  M)
+-- U_T     Functor Kleisli A
+-- U_T     FObj = λ B → Σ (Carrier M) (λ x → B)     FMap = λ {a₁} {b₁} f₁ x → ( proj₁ x ∙ (proj₁ (KMap f₁ (proj₂ x)))  , proj₂ (KMap f₁ (proj₂ x))
+-- F_T     Functor A Kleisli 
+-- F_T     FObj = λ a₁ → a₁                         FMap = λ {a₁} {b₁} f₁ → record { KMap = λ x → ε M , f₁ x }
--- a/yoneda.agda	Sat Aug 31 12:53:35 2013 +0900
+++ b/yoneda.agda	Sun Sep 01 13:26:30 2013 +0900
@@ -1,4 +1,4 @@
-----
+---
 --
 --  A → Sets^A^op  : Yoneda Functor
 --     Contravariant Functor h_a
@@ -23,7 +23,7 @@
 open Functor
 
 YObj = Functor (Category.op A) (Sets {c₂})
-YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g
+YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) (Sets {c₂}) f g
 
 open NTrans 
 Yid : {a : YObj} → YHom a a
@@ -54,23 +54,41 @@
    isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
 
 _==_  :  {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁)
-_==_  f g =  TMap f ≡ TMap g 
+_==_  f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ]
 
 infix  4 _==_
 
 isSetsAop :  IsCategory YObj YHom _==_ _+_ Yid
 isSetsAop  =  
-  record  { isEquivalence =  record {refl = refl ; trans = ≡-trans ; sym = ≡-sym}
+  record  { isEquivalence =  record {refl = refl ; trans = \{i j k} → trans1 {_} {_} {i} {j} {k} ; sym = \{i j} → sym1  {_} {_} {i} {j}}
         ; identityL = refl
         ; identityR = refl
         ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈      {a} {b} {c} {f} {g} {h} {i}
         ; associative = refl
         } where
+            sym1 : {a b : YObj } {i j : YHom a b } → i == j → j == i
+            sym1 {a} {b} {i} {j} eq {x} = let open ≈-Reasoning (Sets {c₂}) in begin
+                 TMap j x
+             ≈⟨ sym eq ⟩
+                 TMap i x
+             ∎ 
+            trans1 : {a b : YObj } {i j k : YHom a b} → i == j → j == k → i == k
+            trans1 {a} {b} {i} {j} {k} i=j j=k {x} =  let open ≈-Reasoning (Sets {c₂}) in begin
+                 TMap i x
+             ≈⟨ i=j ⟩
+                 TMap j x
+             ≈⟨ j=k ⟩
+                 TMap k x
+             ∎
             o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → 
                 f == g → h == i → h + f == i + g
-            o-resp-≈ refl refl =  refl
+            o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = let open ≈-Reasoning (Sets {c₂}) in begin
+                 (Sets {c₂}) [ TMap h x  o TMap f x ]
+             ≈⟨ resp f=g h=i ⟩
+                 (Sets {c₂}) [ TMap i x  o TMap g x ]
+             ∎
 
-SetsAop : Category (suc (ℓ ⊔ (suc c₂) ⊔ c₁)) (suc ( ℓ ⊔ (suc c₂) ⊔ c₁))  (c₂ ⊔ c₁)
+SetsAop : Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁)
 SetsAop =
   record { Obj = YObj
          ; Hom = YHom
@@ -147,8 +165,6 @@
    isNTrans1 : {a b : Obj A } →  (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) (y-tmap a b f )
    isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } 
 
-postulate extensionality1 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂
-
 -----
 --
 -- Yoneda Functor itself
@@ -167,32 +183,29 @@
         } 
   } where
         ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ]
-        ≈-cong {a} {b} {f} {g} eq =  let open ≈-Reasoning (A) in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
-           extensionality1 ( λ x → extensionality (
-             λ h →  ≈-≡  ( begin
+        ≈-cong {a} {b} {f} {g} eq  =  let open ≈-Reasoning (A) in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
+             extensionality ( λ h → ≈-≡  ( begin
                 A [ f o h ]
              ≈⟨ resp refl-hom eq ⟩
                 A [ g o h ]
              ∎
-          ) )  )
+          ) ) 
         identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a )  ]
         identity  {a} =  let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
-           extensionality1 ( λ x → extensionality (
-             λ g →  ≈-≡  ( begin
+             extensionality ( λ g →  ≈-≡  ( begin
                 A [ id1 A a o g ] 
              ≈⟨ idL ⟩
                 g
              ∎
-          ) )  )
+          ) )  
         distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-map (A [ g o f ]) ≈ SetsAop [ y-map g o y-map f ] ]
         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]))) ≡ (λ x x₁ → A [  g o A [ f o x₁ ] ] )
-           extensionality1 ( λ x → extensionality (
-             λ h →  ≈-≡  ( begin
+           extensionality ( λ h →  ≈-≡  ( begin
                 A [ A [ g o f ]  o h ]
              ≈↑⟨ assoc  ⟩
                 A [  g o A [ f o h ] ]
              ∎
-          ) )  )
+          ) )  
 
 
 ------
@@ -249,18 +262,19 @@
 
 open  import  Relation.Binary.PropositionalEquality
 
-postulate extensionality2 : Relation.Binary.PropositionalEquality.Extensionality  c₁ c₂ 
-postulate extensionality3 : Relation.Binary.PropositionalEquality.Extensionality  c₂ c₂
+≡-cong = Relation.Binary.PropositionalEquality.cong 
 
 --     F :  op A → Sets
 --     ha : NTrans (op A) Sets (y-obj {a}) F
 --                FMap F  g  o TMap ha a ≈   TMap ha b  o FMap (y-obj {a}) g
 
 Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (y-obj a) F) →  SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ]
-Nat2F→F2Nat {a} {F} ha = let open ≡-Reasoning in
+Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in
              begin
-                ( λ (b : Obj A ) → λ (g : Hom A b a ) → FMap F g (TMap ha a (Category.Category.Id A))  )
-             ≡⟨ extensionality2 ( λ b → extensionality3 (λ g → (
+                TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b
+             ≡⟨⟩
+                (λ g → FMap F g (TMap ha a (Category.Category.Id A)))
+             ≡⟨  extensionality (λ g → (
                 begin
                     FMap F g (TMap ha a (Category.Category.Id A)) 
                 ≡⟨  Relation.Binary.PropositionalEquality.cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩
@@ -270,8 +284,8 @@
                 ≡⟨  Relation.Binary.PropositionalEquality.cong ( TMap ha b ) ( ≈-≡ (IsCategory.identityL  ( Category.isCategory A ))) ⟩
                     TMap ha b g
                 ∎ 
-             ))) ⟩
-                TMap ha   
+             )) ⟩
+                TMap ha b
              ∎ 
 
 -- Yoneda's Lemma
@@ -299,7 +313,10 @@
 -- equive-hom : {a b : Obj A } → {f : Hom A a b } → Hom A a b  ≡ Hom A a a → a ≡ b 
 -- equive-hom  {a} {b} {f} eq  = {!!}
 
--- YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →  
---        {f : Hom A a b } → a ≡ b 
--- YondaLemma2 {a} {b} eq  {f}  = {!!} eq
+--YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →  
+--       {f : Hom A a b } → a ≡ b 
+--YondaLemma2 {a} {b} eq  {f}  = ≡-cong (Category.cod ? ) eq
+
+-- inv-yobj =  {a x : Obj A} →  Category.cod A (( FObj (FObj YonedaFunctor a) x))
+
 -- I cannot prove this, please help.