Mercurial > hg > Members > kono > Proof > category

changeset 628:b99660fa14e1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove arrow's yellow
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Jun 2017 17:18:23 +0900
parents efa1f2103a83
children 693020c766d2
files freyd.agda freyd2.agda
diffstat 2 files changed, 18 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Sun Jun 25 13:03:33 2017 +0900
+++ b/freyd.agda	Mon Jun 26 17:18:23 2017 +0900
@@ -1,8 +1,7 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 
-module freyd {c₁ c₂ ℓ : Level} 
-  where
+module freyd where
 
 open import cat-utility
 open import HomReasoning
@@ -24,10 +23,11 @@
 -- pre-initial
 
 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (F : Functor A A )  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+      {preini : Obj A} (F : Functor A A)  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      preinitialObj : Obj A 
-      preinitialArrow : ∀{  a : Obj A } →  Hom A ( FObj F (preinitialObj)) a 
+      preinitialArrow : ∀{a : Obj A } →  Hom A ( FObj F preini) a 
+   preinitialObj : Obj A 
+   preinitialObj = preini
 
 -- initial object
 
@@ -50,7 +50,7 @@
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
       (SFS : SmallFullSubcategory A ) → 
-      (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
+      (PI : PreInitial A {limit-c comp (SFSF SFS)} (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	Sun Jun 25 13:03:33 2017 +0900
+++ b/freyd2.agda	Mon Jun 26 17:18:23 2017 +0900
@@ -185,7 +185,7 @@
 
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
-      → HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
+      → HasInitialObject  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
            initial =  λ b → initial0 b
          ; uniqueness =  λ b f → unique b f
@@ -247,21 +247,23 @@
 
 ≡-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 {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A * ↓ U) )  
-     (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A * ↓ U) (SFSF SFS )) 
+     (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )  
+     (pi : Obj ( K (Sets) A * ↓ U) )
+     (PI : PreInitial ( K (Sets) A * ↓ U) {pi} (SFSF SFS)) 
        → Representable A U (obj (preinitialObj PI ))
-UisRepresentable A U SFS PI = record {
+UisRepresentable A U SFS pi PI = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
-        ; reprId→  = λ {y}  →　?
-        ; reprId←  = λ {y}  →　?
+        ; reprId→  = {!!}
+        ; reprId←  = {!!}
    } where
-      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 (preinitialObj PI))) b)
-      tmap1 b x =  arrow ( SFSFMap← SFS ( preinitialArrow PI ) )  
+      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}) } ))  
       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 )
       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 ] ]