Mercurial > hg > Members > kono > Proof > category

changeset 644:8e35703ef116

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
representability theorem done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jul 2017 15:35:28 +0900
parents 5eb746702732
children 5f26af3f1c00
files freyd2.agda
diffstat 1 files changed, 1 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Mon Jul 03 12:20:26 2017 +0900
+++ b/freyd2.agda	Mon Jul 03 15:35:28 2017 +0900
@@ -246,7 +246,7 @@
 
             
 
--- A is complete and K{*}↓U has preinitial full subcategory then U is representable
+-- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable
 
 open SmallFullSubcategory
 open PreInitial
@@ -284,63 +284,6 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
-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 → limitInSets Γ lim
-   } where
-       limitInSets : (Γ : Functor I A) (lim : Limit A I Γ) →
-          IsLimit Sets I (U ○ Γ) (FObj U (a0 lim)) (LimitNat A I Sets Γ (a0 lim) (t0 lim) U)
-       limitInSets Γ 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 
-         } where
-               lim-t0 : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
-                  → NTrans I A (K A I (a0 lim)) Γ
-               lim-t0 a t x {y} {z} {f} = t0 lim
-               lim-t0-comm : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
-                  → A [ A [ FMap Γ f o TMap (t0 lim) y ] ≈ A [ TMap (t0 lim) z o FMap (K A I (a0 lim)) f ] ]
-               lim-t0-comm a t x {y} {z} {f} = IsNTrans.commute (isNTrans (t0 lim))
-               revU : (a : Obj (K Sets A * ↓ U)) 
-                  → Sets [ Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) o hom (preinitialObj PI) ] ≈ hom a ]
-               revU a  =  let open ≈-Reasoning Sets in begin
-                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) o hom (preinitialObj PI)
-                  ≈⟨ comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ⟩
-                     hom a
-                  ∎ 
-               tacomm0 : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
-                  → Sets [ Sets [ FMap (U ○ Γ) f o TMap t y ] ≈ Sets [ TMap t z o FMap ( K Sets I a ) f ] ]
-               tacomm0 a t x {y} {z} {f} = IsNTrans.commute ( isNTrans t )  {y} {z} {f}
-               tacomm : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
-                  → A [ A [ FMap Γ f o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) ] ≈
-                        A [ arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
-                            o FMap (K A I (obj (preinitialObj PI))) f ] ]
-               tacomm a t x {y} {z} {f} = let open ≈-Reasoning A in begin
-                    FMap Γ f o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) 
-                 ≈⟨ {!!} ⟩
-                    arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (FMap U (FMap Γ f) (TMap t y x)))} ))
-                 ≈⟨ {!!} ⟩
-                    arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
-                 ≈↑⟨ idR ⟩
-                    arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
-                            o FMap (K A I (obj (preinitialObj PI))) f 
-                 ∎
-               ta : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) → NTrans I A (K A I (obj (preinitialObj PI))) Γ
-               ta a t x = record {  TMap = λ (a : Obj I ) →
-                   arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ a) (TMap t a x))} ) )
-                ; isNTrans = record { commute = λ {y} {z} {f} → tacomm a t x {y} {z} {f} }} 
-               ψ : (a : Obj Sets) → NTrans I Sets (K Sets I a) (U ○ Γ) → Hom Sets a (FObj U (a0 lim))
-               ψ a t x = FMap U (limit (isLimit lim) (obj (preinitialObj PI)) (ta a t x)) ( hom (preinitialObj PI) OneObj )
-               t0f=t0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (U ○ Γ)} {i : Obj I} →
-                   Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) U) i o ψ a t ] ≈ TMap t i ]
-               t0f=t0 {a} {t} = {!!}
-               limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (U ○ Γ)} {f : Hom Sets a (FObj U (a0 lim))} →
-                   ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) U) i o f ] ≈ TMap t i ]) → Sets [ ψ a t ≈ f ]
-               limit-uniqueness0 {a} {t} {f} = {!!}
 
 -- if K{*}↓U has initial Obj, U is representable