Mercurial > hg > Members > kono > Proof > category

changeset 629:693020c766d2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Jun 2017 17:41:02 +0900
parents b99660fa14e1
children d2fc6fb58e0e
files freyd.agda freyd2.agda
diffstat 2 files changed, 32 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Mon Jun 26 17:18:23 2017 +0900
+++ b/freyd.agda	Mon Jun 26 17:41:02 2017 +0900
@@ -23,11 +23,10 @@
 -- pre-initial
 
 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      {preini : Obj A} (F : Functor A A)  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+       (F : Functor A A)  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      preinitialArrow : ∀{a : Obj A } →  Hom A ( FObj F preini) a 
-   preinitialObj : Obj A 
-   preinitialObj = preini
+      preinitialObj : Obj A 
+      preinitialArrow : ∀{a : Obj A } →  Hom A ( FObj F preinitialObj ) a 
 
 -- initial object
 
@@ -50,7 +49,7 @@
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
       (SFS : SmallFullSubcategory A ) → 
-      (PI : PreInitial A {limit-c comp (SFSF SFS)} (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
+      (PI : PreInitial A  (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
 initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
--- a/freyd2.agda	Mon Jun 26 17:18:23 2017 +0900
+++ b/freyd2.agda	Mon Jun 26 17:41:02 2017 +0900
@@ -247,29 +247,50 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong
 
-ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
-ub A U b x OneObj = x
 
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
      (U : Functor A (Sets {c₂}) )
      (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )  
-     (pi : Obj ( K (Sets) A * ↓ U) )
-     (PI : PreInitial ( K (Sets) A * ↓ U) {pi} (SFSF SFS)) 
+     (PI : PreInitial ( K (Sets) A * ↓ U)  (SFSF SFS)) 
        → Representable A U (obj (preinitialObj PI ))
-UisRepresentable A U SFS pi PI = record {
+UisRepresentable A U SFS PI = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
         ; reprId→  = {!!}
         ; reprId←  = {!!}
    } where
+      pi : Obj ( K (Sets) A * ↓ U) 
+      pi = preinitialObj PI
+      ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
+      ub b x OneObj = x
       tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
-      tmap1 b x =  arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub A U b x}) } ))  
+      tmap1 b x =  arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))  
       tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
       tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
+      comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
+         ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o
+             ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y   
+           ≡ (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y
+      comm11 a b f y = begin
+               ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o
+                 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y   
+             ≡⟨⟩
+                 A [ f o arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a y}) } )) ]
+             ≡⟨ {!!} ⟩
+                arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b (FMap U f y) } ) } ) )
+             ≡⟨⟩
+                (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y
+             ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
       comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
       comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
                 FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a 
-             ≈⟨ {!!} ⟩
+             ≈⟨⟩
+                FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } )))  
+             ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
+                ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f 
+             ≈⟨⟩
                 tmap1 b o FMap U f 
              ∎ 
       comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) →