Mercurial > hg > Members > kono > Proof > category

changeset 638:a07b95e92933

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
creating nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Jul 2017 10:21:34 +0900
parents 946ea019a2e7
children 4cf8f982dc5b
files freyd2.agda
diffstat 1 files changed, 93 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Sat Jul 01 00:12:38 2017 +0900
+++ b/freyd2.agda	Sat Jul 01 10:21:34 2017 +0900
@@ -245,16 +245,87 @@
 open SmallFullSubcategory
 open PreInitial
 
+-- if U preserve limit,  K{*}↓U has initial object from freyd.agda
+
 ≡-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
+ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
+   → Obj ( K Sets A * ↓ U)
+ob A U b x = record { obj = b ; hom = ub A U b x}
+fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )  {a b : Obj A} (f : Hom A a b) (x : FObj U a )
+   → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) )
+fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
+  where
+        fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y
+        fArrowComm1 a b f x OneObj = refl
+        fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → 
+         Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ]
+        fArrowComm a b f x = extensionality Sets ( λ y → begin 
+                ( Sets [ FMap U f o hom (ob A U a x) ] ) y 
+             ≡⟨⟩
+                FMap U f ( hom (ob A U a x) y )
+             ≡⟨⟩
+                FMap U f ( ub A U a x y )
+             ≡⟨ fArrowComm1 a b f x y ⟩
+                ub A U b (FMap U f x) y
+             ≡⟨⟩
+                hom (ob A U b (FMap U f x)) y
+             ∎ ) where
+                  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 → {!!} -- UpreserveLimit0 A I b Γ lim
-   } 
+       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
+               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 (fArrow A U (FMap Γ f) (TMap t y x )) 
+                        o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) 
+                 ≈⟨ {!!} ⟩
+                    arrow (SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) ))
+                        o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) 
+                 ≈⟨ {!!} ⟩
+                    arrow (SFSFMap← SFS (( K (Sets) A * ↓ U) [ FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) 
+                        o 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) (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 = {!!} }} -- λ {a} {b} {f} → commute2 {a} {b} {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
 
@@ -266,57 +337,34 @@
 UisRepresentable A U i In = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
-        ; reprId→  = {!!}
-        ; reprId←  = {!!}
+        ; reprId→  = iso→ 
+        ; reprId←  = iso←
    } where
-      ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
-      ub b x OneObj = x
-      ob : (b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U)
-      ob b x = record { obj = b ; hom = ub b x}
-      fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y
-      fArrowComm1 a b f x OneObj = refl
-      fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → 
-         Sets [ Sets [ FMap U f o hom (ob a x) ] ≈ Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ]
-      fArrowComm a b f x = extensionality Sets ( λ y → begin 
-                ( Sets [ FMap U f o hom (ob a x) ] ) y 
-             ≡⟨⟩
-                FMap U f ( hom (ob a x) y )
-             ≡⟨⟩
-                FMap U f ( ub a x y )
-             ≡⟨ fArrowComm1 a b f x y ⟩
-                ub b (FMap U f x) y
+      comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
+         ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y   
+           ≡ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
+      comm11 a b f y = begin
+               ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y   
              ≡⟨⟩
-                hom (ob b (FMap U f x)) y
-             ∎ ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-      fArrow :  {a b : Obj A} (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
-      fArrow {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
-      comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
-         ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob a x))) ] ) y   
-           ≡ (Sets [ ( λ x → arrow (initial In (ob b x))) o FMap U f ] ) y
-      comm11 a b f y = begin
-               ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob a x))) ] ) y   
+                 A [ f o arrow (initial In (ob A U a y)) ]
              ≡⟨⟩
-                 A [ f o arrow (initial In (ob a y)) ]
+                 A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ]
+             ≡⟨  ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y  o initial In (ob A U a y)] ) ) ⟩
+                arrow (initial In (ob A U b (FMap U f y) ))
              ≡⟨⟩
-                 A [ arrow ( fArrow f y ) o arrow (initial In (ob a y)) ]
-             ≡⟨  ≈-≡ A ( uniqueness In {ob b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow f y  o initial In (ob a y)] ) ) ⟩
-                arrow (initial In (ob b (FMap U f y) ))
-             ≡⟨⟩
-                (Sets [ ( λ x → arrow (initial In (ob b x))) o FMap U f ] ) y
+                (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
              ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
       tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b)
-      tmap1 b x = arrow ( initial In (ob b x ) ) 
+      tmap1 b x = arrow ( initial In (ob A U b x ) ) 
       comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
       comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
                 FMap (Yoneda A (obj i)) f o tmap1 a 
              ≈⟨⟩
-                FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob a x )))  
+                FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob A U a x )))  
              ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
-                ( λ x → arrow (initial In (ob b x))) o FMap U f 
+                ( λ x → arrow (initial In (ob A U b x))) o FMap U f 
              ≈⟨⟩
                 tmap1 b o FMap U f 
              ∎ 
@@ -346,13 +394,13 @@
                 tmap2 b o FMap (Yoneda A (obj i)) f 
              ∎
       iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * )
-         → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z 
+         → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z 
       iso0 x y  OneObj = refl
       iso→  : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ]
       iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin
                ( Sets [ tmap1 x o tmap2 x ] ) y
              ≈⟨⟩
-                arrow ( initial In (ob x (( FMap U y ) ( hom i OneObj ) ))) 
+                arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) ))) 
              ≈↑⟨  uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) }  ) ⟩
                y
              ∎  ))
@@ -360,9 +408,9 @@
       iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin 
                ( Sets [ tmap2 x o tmap1 x ] ) y
              ≡⟨⟩
-               ( FMap U ( arrow ( initial In (ob x y ) ))  ) ( hom i OneObj )
-             ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob x y ) )) ⟩
-                 hom (ob x y) OneObj
+               ( FMap U ( arrow ( initial In (ob A U x y ) ))  ) ( hom i OneObj )
+             ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob A U x y ) )) ⟩
+                 hom (ob A U x y) OneObj
              ≡⟨⟩
                y
              ∎  ) ) where