Mercurial > hg > Members > kono > Proof > category

changeset 617:34540494fdcf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initital obj uniquness done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Jun 2017 18:49:21 +0900
parents 7011165c118e
children 23ff2464f7ad
files freyd.agda freyd2.agda
diffstat 2 files changed, 39 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Wed Jun 14 11:37:48 2017 +0900
+++ b/freyd.agda	Mon Jun 19 18:49:21 2017 +0900
@@ -26,8 +26,8 @@
 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
       (F : Functor A A )  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      preinitialObj : ∀{  a : Obj A } →  Obj A 
-      preinitialArrow : ∀{  a : Obj A } →  Hom A ( FObj F (preinitialObj {a} )) a 
+      preinitialObj : Obj A 
+      preinitialArrow : ∀{  a : Obj A } →  Hom A ( FObj F (preinitialObj)) a 
 
 -- initial object
 
@@ -71,8 +71,8 @@
       ep {a} {b} {f} {g} = equalizer-p comp f g
       ee :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ep {a} {b} {f} {g} ) a 
       ee {a} {b} {f} {g} = equalizer-e comp f g  
-      f : {a : Obj A} → Hom A  a00 (FObj F  (preinitialObj PI {a} ) ) 
-      f {a} = TMap u (preinitialObj PI {a} ) 
+      f : Hom A  a00 (FObj F  (preinitialObj PI ) ) 
+      f = TMap u (preinitialObj PI ) 
       initialArrow :  ∀( a : Obj A )  →  Hom A a00 a
       initialArrow a  = A [ preinitialArrow PI {a}  o f ]
       equ-fi : { a : Obj A} → {f' : Hom A a00 a} → 
--- a/freyd2.agda	Wed Jun 14 11:37:48 2017 +0900
+++ b/freyd2.agda	Mon Jun 19 18:49:21 2017 +0900
@@ -29,6 +29,7 @@
 
 open Small
 
+-- maybe this is a part of local smallness
 postulate ≈-≡ :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
 import Relation.Binary.PropositionalEquality
@@ -38,7 +39,7 @@
 
 ----
 --
---  Hom ( a, - ) is Object mapping in co Yoneda Functor
+--  Hom ( a, - ) is Object mapping in Yoneda Functor
 --
 ----
 
@@ -111,7 +112,7 @@
 -- Representable Functor U preserve limit , so K{*}↓U is complete
 --
 --    Yoneda A b =  λ a → Hom A a b    : Functor A Sets
---                                   : Functor Sets A
+--                                     : Functor Sets A
 
 UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
       (b : Obj A ) 
@@ -188,12 +189,14 @@
 -- K{*}↓U has preinitial full subcategory if U is representable
 --     if U is representable,  K{*}↓U has initial Object ( so it has preinitial full subcategory )
 
+open CommaHom
+
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
       → 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 → {!!}
+         ; uniqueness =  λ b f → unique b f
      } where
          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
@@ -202,6 +205,8 @@
              ≈⟨⟩
                hom b (id1 A a ) o x
              ≈⟨ {!!} ⟩
+               hom b (id1 A a  o x )
+             ≈⟨ ≡-≈ ( cong (λ k → hom b k ) ( ≈-≡ A idL )  ) ⟩
                hom b x
              ∎ )
          initial0com :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →
@@ -224,19 +229,40 @@
          initial0 b = record {
                 arrow = hom b (id1 A a) 
               ; comm = initial0com b }
+         comm-f :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a)))
+            (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b)
+            → Sets [ Sets [ FMap  (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ]
+            ≈ Sets [ hom b  o  FMap  (K Sets A (FObj (Yoneda A a) a)) (arrow f) ]  ] 
+         comm-f b f = comm f
+         unique : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a))
+                (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b)
+                → (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) [ f ≈ initial0 b ]
+         unique b f = let open ≈-Reasoning A in begin
+                arrow f
+             ≈↑⟨ idR ⟩
+                arrow f o id1 A a
+             ≈⟨⟩
+                ( Sets [ FMap  (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a)  ] ) (id1 A a)
+             ≈⟨ ≡-≈ ( cong (λ k → k (id1 A a)) (comm f ) ) ⟩
+               ( Sets [ hom b  o  FMap  (K Sets A (FObj (Yoneda A a) a)) (arrow f) ]  ) (id1 A a)
+             ≈⟨⟩
+                hom b (id1 A a)
+             ∎ 
             
 
 -- K{*}↓U has preinitial full subcategory then U is representable
 --    K{*}↓U is complete, so it has initial object
 
+open SmallFullSubcategory
+open PreInitial
+
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-      (comp : Complete A A)
       (U : Functor A (Sets {c₂}) )
-      (a : Obj Sets )
-      (x : Obj ( K (Sets) A a ↓ U) )
-      ( init : HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U ) x )
-        → Representable A U (obj x)
-UisRepresentable A comp U a x init = record {
+      (a : Obj (Sets {c₂}))
+      (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) )  
+      (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS )) 
+        → Representable A U (obj (preinitialObj PI ))
+UisRepresentable A U a SFS PI = record {
          repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
          ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } }
          ; reprId→  = λ {y}  →　?