Mercurial > hg > Members > kono > Proof > category

changeset 641:c65d08d85092

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add revU
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jul 2017 07:26:58 +0900
parents 0d6cab67eadc
children 53f2a11474ee
files freyd2.agda
diffstat 1 files changed, 19 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Sun Jul 02 10:17:26 2017 +0900
+++ b/freyd2.agda	Mon Jul 03 07:26:58 2017 +0900
@@ -88,6 +88,12 @@
 _↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } F G  = CommaCategory
          where open import Comma1 F G
 
+natf :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
+    →  { F G : Functor A B }
+    → Functor A B  → Functor A (F ↓ G) → Functor A B
+natf   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } {F} {G} H I = nat-f H I
+         where open import Comma1 F G
+
 open import freyd
 open SmallFullSubcategory
 open Complete
@@ -280,8 +286,8 @@
 
 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)) 
+     (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
@@ -293,38 +299,26 @@
                ; 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
+               revU : (a : Obj (K Sets A * ↓ U)) 
+                  → Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) ≈ ( λ upi → hom a OneObj ) ]
+               revU a  = extensionality Sets ( λ (pi : FObj U (obj (preinitialObj PI)) ) → ( begin 
+                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) pi  
+                  ≡⟨ {!!} ⟩
+                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) (hom (preinitialObj PI) OneObj)
+                  ≡⟨ ≡-cong ( λ k → k OneObj ) ( comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) ⟩
+                     hom a OneObj
+                ∎  ) ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
                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}
-               sfcomm : (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 ( arrow (FMap (SFSF SFS) (fArrow A U (FMap Γ f) (TMap t y x))))
-                        o hom (FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))) ]
-                     ≈ Sets [ hom (FObj (SFSF SFS) (ob A U (FObj Γ z) (FMap U (FMap Γ f) (TMap t y x)))) o
-                          FMap ( K Sets A * ) ( arrow (FMap (SFSF SFS) (fArrow A U (FMap Γ f) (TMap t y x)))) ] ]
-               sfcomm a t x {y} {z} {f} = comm (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) )
-               commacomm : (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} 
-                  → ( K (Sets) A * ↓ U) [ ( 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))} ]
-                     ≈ preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (FMap U (FMap Γ f) (TMap t y x))) } ]
-               commacomm = {!!}
                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 (( K (Sets) A * ↓ U) [ SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) )
-                        o 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) (FMap U (FMap Γ f) (TMap t y x)))} ))
                  ≈⟨ {!!} ⟩