Mercurial > hg > Members > kono > Proof > category

changeset 616:7011165c118e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 14 Jun 2017 11:37:48 +0900
parents a45c32ceca97
children 34540494fdcf
files freyd2.agda
diffstat 1 files changed, 49 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Wed Jun 14 10:37:41 2017 +0900
+++ b/freyd2.agda	Wed Jun 14 11:37:48 2017 +0900
@@ -48,8 +48,8 @@
 open IsLimit
 open import Category.Cat
 
-HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
-HomA  {c₁} {c₂} {ℓ} A a = record {
+Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
+Yoneda  {c₁} {c₂} {ℓ} A a = record {
     FObj = λ b → Hom A a b
   ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ]    --   f : Hom A x y  → Hom Sets (Hom A a x ) (Hom A a y)
   ; isFunctor = record {
@@ -85,9 +85,9 @@
          -- λ b → Hom (a,b) :  A → Set
          -- λ f → Hom (a,-) = λ b → Hom  a b    
 
-         repr→ : NTrans A (Sets {c₂}) U (HomA A a )
-         repr← : NTrans A (Sets {c₂}) (HomA A a)  U
-         reprId→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A a) x )]
+         repr→ : NTrans A (Sets {c₂}) U (Yoneda A a )
+         repr← : NTrans A (Sets {c₂}) (Yoneda A a)  U
+         reprId→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )]
          reprId←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
 
 open Representable
@@ -110,30 +110,30 @@
 
 -- Representable Functor U preserve limit , so K{*}↓U is complete
 --
---    HomA A b =  λ a → Hom A a b    : Functor A Sets
+--    Yoneda A b =  λ a → Hom A a b    : Functor A Sets
 --                                   : Functor Sets A
 
 UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
       (b : Obj A ) 
       (Γ : Functor I A) (limita : Limit A I Γ) →
-        IsLimit Sets I (HomA A b ○ Γ) (FObj (HomA A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b))
+        IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b))
 UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record {
          limit = λ a t → ψ a t
        ; t0f=t = λ {a t i} → t0f=t0 a t i
        ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t 
     } where 
-      hat0 :  NTrans I Sets (K Sets I (FObj (HomA A b) (a0 lim))) (HomA A b ○ Γ)
-      hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)
+      hat0 :  NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ)
+      hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)
       haa0 : Obj Sets
-      haa0 = FObj (HomA A b) (a0 lim)
-      ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) → NTrans I A (K A I b ) Γ
+      haa0 = FObj (Yoneda A b) (a0 lim)
+      ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ
       ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where
          commute1 :  {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} →
                 A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ]  ]
          commute1  {a₁} {b₁} {f} = let open ≈-Reasoning A in begin
                  FMap Γ f o TMap t a₁ x
              ≈⟨⟩
-                 ( ( FMap (HomA A b  ○ Γ ) f )  *  TMap t a₁ ) x
+                 ( ( FMap (Yoneda A b  ○ Γ ) f )  *  TMap t a₁ ) x
              ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩
                  ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x
              ≈⟨⟩
@@ -145,15 +145,15 @@
              ≈⟨⟩
                  TMap t b₁ x o FMap (K A I b) f 
              ∎ 
-      ψ  :  (X : Obj Sets)  ( t : NTrans I Sets (K Sets I X) (HomA A b ○ Γ))
-          →  Hom Sets X (FObj (HomA A b) (a0 lim))
-      ψ X t x = FMap (HomA A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
-      t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) (i : Obj I)
-           → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ≈ TMap t i ]
+      ψ  :  (X : Obj Sets)  ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ))
+          →  Hom Sets X (FObj (Yoneda A b) (a0 lim))
+      ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
+      t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I)
+           → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ]
       t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
-                 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t  ] ) x
+                 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t  ] ) x
              ≈⟨⟩
-                FMap (HomA A b) ( TMap (t0 lim) i) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
+                FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
              ≈⟨⟩ -- FMap (Hom A b ) f g  = A [ f o g  ]
                 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b )
              ≈⟨  cdr idR ⟩
@@ -163,13 +163,13 @@
              ≈⟨⟩
                  TMap t i x
              ∎  ))
-      limit-uniqueness0 :  {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)} {f : Hom Sets a (FObj (HomA A b) (a0 lim))} →
-        ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o f ] ≈ TMap t i ]) →
+      limit-uniqueness0 :  {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} →
+        ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) →
         Sets [ ψ a t ≈ f ]
       limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
                   ψ a t x
              ≈⟨⟩
-                 FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )
+                 FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )
              ≈⟨⟩
                  limit (isLimit lim) b (ta a x t ) o id1 A b 
              ≈⟨ idR ⟩
@@ -180,7 +180,7 @@
 
 
 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-       (b : Obj A ) → LimitPreserve A I Sets (HomA A b) 
+       (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) 
 UpreserveLimit A I b = record {
        preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
    } 
@@ -189,31 +189,40 @@
 --     if U is representable,  K{*}↓U has initial Object ( so it has preinitial full subcategory )
 
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-      (comp : Complete A A)
-      (U : Functor A (Sets) )
       (a : Obj A )
-      (R : Representable A U a ) →
-      HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A (FObj U a) ↓ U ) ( record  { obj = a ; hom = id1 Sets (FObj U a) } )
-KUhasInitialObj A comp U a R = record {
+      → HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A (FObj (Yoneda A a) a) ↓ (Yoneda A a) ) ( record  { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) } )
+KUhasInitialObj A a = record {
            initial =  λ b → initial0 b
          ; uniqueness =  λ b f → {!!}
      } where
-         initial0com :  (b : Obj (K Sets A (FObj U a) ↓ U)) →
-              Sets [ Sets [ FMap U (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) o id1 Sets (FObj U a) ]
-                 ≈ Sets [ hom b o FMap (K Sets A (FObj U a)) (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) ] ]
-         initial0com b = let open ≈-Reasoning Sets in begin
-                   FMap U (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) o id1 Sets (FObj U a)
+         initial0com1 :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x :  FObj (Yoneda A a) a )
+            →  FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x
+         initial0com1 b x =  let open ≈-Reasoning A in ≈-≡ A ( begin
+               FMap (Yoneda A a) (hom b (id1 A a)) x  
              ≈⟨⟩
-                   FMap U (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a)))) 
+               hom b (id1 A a ) o x
              ≈⟨ {!!} ⟩
-                   hom b o FMap (K Sets A (FObj U a)) (TMap (repr→ R) (obj b) (hom b (TMap (repr← R) a (id1 A a))))
+               hom b x
+             ∎ )
+         initial0com :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
+            Sets [ Sets [ FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) ] ≈
+                Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) ] ]
+         initial0com b = let open ≈-Reasoning Sets in begin
+                   FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) 
+             ≈⟨⟩
+                   FMap (Yoneda A a) (hom b (id1 A a)) 
+             ≈⟨ extensionality A ( λ x → initial0com1 b x ) ⟩
+                   hom b 
+             ≈⟨⟩
+                   hom b o id1 Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b))
+             ≈⟨⟩
+                   hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) 
              ∎ 
-
-         initial0 : (b : Obj (K Sets A (FObj U a) ↓ U)) →
-            Hom ((K Sets A (FObj U a)) ↓ U)
-              (record { obj = a ; hom = id1 Sets (FObj U a) }) b
+         initial0 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
+            Hom ((K Sets A (FObj (Yoneda A a) a)) ↓ (Yoneda A a))
+              (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b
          initial0 b = record {
-                arrow =   TMap ( repr→ R ) (obj b) ( hom b (TMap ( repr← R ) a (id1 A a)))
+                arrow = hom b (id1 A a) 
               ; comm = initial0com b }