Mercurial > hg > Members > kono > Proof > category

changeset 526:b035cd3be525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Small Category for Sets Limit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Mar 2017 11:49:35 +0900
parents cb35d6b25559
children beac7b0786cb
files SetsCompleteness.agda cat-utility.agda
diffstat 2 files changed, 34 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Mar 27 10:18:08 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 28 11:49:35 2017 +0900
@@ -146,38 +146,37 @@
 open Functor
 open NTrans
 
-record ΓObj   { c₂ }  ( I   : Set  c₂ )    : Set  c₂ where
+record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
+                : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-     obj :  I
-
-open ΓObj
+     small→ : Obj C → I
+     small← : I → Obj C
+     small-iso : { i : I } → small→ ( small← i ) ≡ i
+     shom→ : {i j : Obj C  } →    Hom C i j →  I → I 
+     shom← : {i j : I } →  ( f : I → I ) →  Hom C ( small←  i  ) (  small←  j )
+     shom-iso : {i j : I } →  ( f : Hom C ( small←  i  ) (  small←  j ) ) →  C [ shom← ( shom→ f )  ≈ f ]
 
-record ΓMap   { c₂ }  {a b :  Set  c₂ } ( f : a → b )  : Set  c₂ where
-   field
-     map : ΓObj a → ΓObj b
+open Small 
 
-open ΓMap
+ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
+   (i : I ) →　 Set c₁
+ΓObj s  Γ i = FObj Γ (small← s i )
 
-fmap : { c₂ : Level}   {a b :  Set  c₂ } → (f : a → b  ) → ΓMap f
-fmap {a} {b} f =  record { map = λ aobj →  record { obj = f ( obj aobj ) } } 
-Γ :  { c₂ : Level } → Functor  (Sets { c₂}) (Sets { c₂}) 
-Γ { c₂} =   record { FObj =  ΓObj ; FMap = ( λ f →  map (fmap f )) ; isFunctor = record {
-         identity =  λ {b} → refl ;
-         distr = λ {a} {b} {c} {f} {g} → refl ;
-         ≈-cong = cong1
-    } } where
-       cong1 :  {A B : Obj Sets} {f g : Hom Sets A B} → Sets [ f ≈ g ] → Sets [ map (fmap f) ≈ map (fmap g) ]
-       cong1 refl =  refl 
+ΓMap :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
+    {i j : I } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
+ΓMap  s Γ {i} {j} f = FMap Γ ( shom← s f ) 
+
+
+record slim   { c₂ }  { I :  Set  c₂ } ( sobj :  I →  Set  c₂ ) 
+     ( smap : { i j :  I  }  → (f : I → I )→  sobj i → sobj j ) : Set  c₂ where
 
-open IProduct
 
-record slim   { c₂ }   ( sobj : Set  c₂ →  Set  c₂ ) ( smap : { a b : Set  c₂ } ( f :  a → b ) → Set  c₂ ) : Set  c₂ where
-
-SetsLimit :  { c₂ : Level}  →  Limit Sets Sets Γ
-SetsLimit { c₂}  = record { 
-           a0 =  slim ΓObj ΓMap
+SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
+    → Limit Sets C Γ
+SetsLimit { c₂} C I s Γ = record { 
+           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
          ; t0 = record { 
-               TMap = λ i → Sets  [ proj i o  e i ]
+               TMap = λ i → {!!}
              ; isNTrans = record { commute = {!!} } 
            }
          ; isLimit = record {
@@ -188,10 +187,9 @@
        }  where
           eqa : {i j : Obj Sets} (f : Hom Sets i j) → sequ (Obj Sets) (Obj Sets) {!!} {!!}         --  {!!} {!!} (FMap Γ f o  proj i) ( proj j ) 
           eqa f = {!!}
-          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets (slim ΓObj ΓMap)) i ) (iproduct (slim ΓObj ΓMap) (λ I → ΓObj (slim ΓObj ΓMap)))
-          e i =  λ x → record { pi1  = λ j → record { obj =  record {}} }
-          proj :  (i : Obj Sets) → ( prod : iproduct (slim ΓObj ΓMap) (λ i → ΓObj (slim ΓObj ΓMap))) → FObj Γ i
-          proj i prod =  record { obj = ? }
-          comm1 :  {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → {!!} ) ] ≈
-                       Sets [ (λ lim → {!!}) o FMap (K Sets Sets {!!}) f ] ]
+          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets (slim  {!!} {!!} )) i ) (iproduct (slim  {!!} {!!} ) (λ I → {!!} (slim  {!!} {!!} )))
+          e i =  λ x → record { pi1  = λ j →  {!!} }
+          proj :  (i : Obj Sets) → ( prod : iproduct (slim   {!!} {!!} ) (λ i → {!!} )) → {!!}
+          proj i prod =  {!!}
+          comm1 :  {a b : Obj Sets} {f : Hom Sets a b} → {!!}
           comm1 {a} {b} {f} = {!!} 
--- a/cat-utility.agda	Mon Mar 27 10:18:08 2017 +0900
+++ b/cat-utility.agda	Tue Mar 28 11:49:35 2017 +0900
@@ -364,10 +364,10 @@
              climit :  ( Γ : Functor I A ) -> Limit A I Γ 
              alimit :  ( Γ : Functor I A ) (a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ )  -> IsLimit A I Γ a0 t0
 
-             product : (a b : Obj A) -> Obj A
-             π1 : (a b : Obj A) -> Hom A (product a b ) a
-             π2 : (a b : Obj A) -> Hom A (product a b ) b
-             isProduct : (a b : Obj A) -> Product A a b (product  a b) (π1 a b ) (π2 a b)
+             -- product : (a b : Obj A) -> Obj A
+             -- π1 : (a b : Obj A) -> Hom A (product a b ) a
+             -- π2 : (a b : Obj A) -> Hom A (product a b ) b
+             -- isProduct : (a b : Obj A) -> Product A a b (product  a b) (π1 a b ) (π2 a b)
 
              equalizer-p : {a b : Obj A} (f g : Hom A a b)  -> Obj A
              equalizer-e : {a b : Obj A} (f g : Hom A a b)  -> Hom A (equalizer-p f g) a
@@ -377,3 +377,4 @@
           limit-c  Γ  = a0 ( climit Γ)
           limit-u :  ( Γ : Functor I A ) ->  NTrans I A ( K A I (limit-c Γ )) Γ
           limit-u  Γ  = t0 ( climit Γ)
+