Mercurial > hg > Members > kono > Proof > category

changeset 499:511fd37d90ec

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prove only limit preserving on co yoneda functor's obj
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Mar 2017 12:28:50 +0900
parents c981a2f0642f
children 6c993c1fe9de
files freyd2.agda
diffstat 1 files changed, 48 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Wed Mar 15 12:10:24 2017 +0900
+++ b/freyd2.agda	Wed Mar 15 12:28:50 2017 +0900
@@ -66,38 +66,64 @@
              ∎ )
 
 
-
-record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
-   field
-         -- FObj U x  :  A  → Set
-         -- FMap U f  =  Set → Set
-         -- λ b → Hom (a,b) :  A → Set
-         -- λ f → Hom (a,-) = λ b → Hom  a b    
-
-         repr→ : NTrans A (Sets {c₂}) U (HomA A b )
-         repr← : NTrans A (Sets {c₂}) (HomA A b)  U
-         representable→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
-         representable←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
-
-UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)
+HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →  (b : Obj A)
       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
-     ( rep :  Representable A U b ) → LimitPreserve A I (Sets  {c₂}) U 
-UpreseveLimit {_} { c₂} A U b I rep =  record {
+      → LimitPreserve A I (Sets  {c₂}) ( HomA A b )
+HpreseveLimit {_} { c₂} A b I =  record {
        preserve = λ Γ limita → record {
              limit = λ a t → limitu a Γ t limita
              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
        }
    } where
-      limitu :   ( a : Obj (Sets  {c₂}) ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →   ( limita : Limit A I Γ  ) →   Hom Sets a (FObj U (a0 limita))
+      limitu :   ( a : Obj Sets ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
+          Hom Sets a (FObj (HomA A b) (a0 limita))
       limitu  = {!!}
-      t0f=tu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
-           ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ]
+      t0f=tu :    { a : Obj  Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
+           ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ]
       t0f=tu  = {!!}
-      limit-uniquenessu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) 
+      limit-uniquenessu :    { a : Obj Sets } → (Γ : Functor I A ) 
            →   ( limita : Limit A I Γ  ) →
-          ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f :  Hom Sets a (FObj U (a0 limita)) ) 
-           →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) )
+          ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f :  Hom Sets a (FObj (HomA A b) (a0 limita)) ) 
+           →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) )
            →  Sets [ limitu a Γ t limita ≈ f ]
       limit-uniquenessu = {!!}
 
+
+
+-- record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
+--    field
+--          -- FObj U x  :  A  → Set
+--          -- FMap U f  =  Set → Set
+--          -- λ b → Hom (a,b) :  A → Set
+--          -- λ f → Hom (a,-) = λ b → Hom  a b    
+-- 
+--          repr→ : NTrans A (Sets {c₂}) U (HomA A b )
+--          repr← : NTrans A (Sets {c₂}) (HomA A b)  U
+--          representable→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
+--          representable←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
+--
+-- 
+-- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)
+--       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
+--      ( rep :  Representable A U b ) → LimitPreserve A I (Sets  {c₂}) U 
+-- UpreseveLimit {_} { c₂} A U b I rep =  record {
+--        preserve = λ Γ limita → record {
+--              limit = λ a t → limitu a Γ t limita
+--              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
+--              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
+--        }
+--    } where
+--       limitu :   ( a : Obj (Sets  {c₂}) ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
+--           Hom Sets a (FObj U (a0 limita))
+--       limitu  = {!!}
+--       t0f=tu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
+--            ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ]
+--       t0f=tu  = {!!}
+--       limit-uniquenessu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) 
+--            →   ( limita : Limit A I Γ  ) →
+--           ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f :  Hom Sets a (FObj U (a0 limita)) ) 
+--            →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) )
+--            →  Sets [ limitu a Γ t limita ≈ f ]
+--       limit-uniquenessu = {!!}
+--