Mercurial > hg > Members > kono > Proof > category

changeset 635:f7cc0ec00e05

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
introduce U preserving
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Jun 2017 21:52:14 +0900
parents 5b0286e3aa32
children 3e663c7f88c4
files freyd2.agda
diffstat 1 files changed, 16 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Wed Jun 28 17:17:17 2017 +0900
+++ b/freyd2.agda	Fri Jun 30 21:52:14 2017 +0900
@@ -102,11 +102,11 @@
 --    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₂ ℓ)
+YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
       (b : Obj A ) 
       (Γ : Functor I A) (limita : Limit A I Γ) →
         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 {
+YonedaFpreserveLimit0 {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 
@@ -168,10 +168,10 @@
              ∎  ))
 
 
-UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
+YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
        (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) 
-UpreserveLimit A I b = record {
-       preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
+YonedaFpreserveLimit A I b = record {
+       preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim
    } 
 
 
@@ -247,6 +247,17 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong
 
+UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
+     (U : Functor A (Sets {c₂}) )
+     (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )  
+     (PI : PreInitial ( K (Sets) A * ↓ U)  (SFSF SFS)) 
+        → LimitPreserve A I Sets U 
+UpreserveLimit A I comp U SFS PI  = record {
+       preserve = λ Γ lim → {!!} -- UpreserveLimit0 A I b Γ lim
+   } 
+
+-- if K{*}↓U has initial Obj, U is representable
+
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( comp : Complete A A )
      (U : Functor A (Sets {c₂}) )
      (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )