Mercurial > hg > Members > kono > Proof > category

changeset 584:f0f516817762

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cequ introduced
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 11 May 2017 14:49:17 +0900
parents cd65d5c9a54d
children 59c3de1c4043
files SetsCompleteness.agda
diffstat 1 files changed, 17 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Wed May 03 18:14:49 2017 +0900
+++ b/SetsCompleteness.agda	Thu May 11 14:49:17 2017 +0900
@@ -178,10 +178,9 @@
 
 record slim  { c₂ }  { I OC :  Set  c₂ } 
                 ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I ) → sobj i → sobj j ) 
-                (lim :   Set  c₂ ) ( e : lim → sproduct OC sobj  ) 
       :  Set   c₂  where
    field 
-       slequ :  (i j : OC) (f :  I → I  ) → sequ lim (sobj j) (λ x →  smap f (proj (e x) i) ) (λ x → proj (e x) j )
+       slequ : ( e : OC → sproduct OC sobj  )  (i j : OC) (f :  I → I  ) → sequ OC (sobj j) (λ x →  smap f (proj (e x) i) ) (λ x → proj (e x) j )
 
 open slim
 
@@ -189,26 +188,31 @@
 open NTrans
 
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
-    → ( lim :  Set  c₁ )
-    → ( e : Hom Sets lim (sproduct (Obj C) (ΓObj s  Γ)) )
-    → NTrans C Sets (K Sets C lim) Γ
-Cone C I s  Γ lim e  =  record {
+    → ( prod :  Set  c₁ → sproduct (Obj C) (ΓObj s Γ) )
+    → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  ) (sproduct (Obj C) (ΓObj s  Γ)  ) )
+    → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)))  Γ
+Cone C I s  Γ prod e  =  record {
                TMap = λ i →  λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s  Γ)}  {FObj Γ i}
                      {λ x → proj x i} {λ x → proj x i} (elem (e se ) refl )) i
              ; isNTrans = record { commute = commute1 }
       } where
-         cone-equ : (a b : Obj C) (f : Hom C a b) → (se : lim ) → sequ lim (FObj Γ b) (λ x →  FMap Γ f (proj (e x) a) ) (λ x → proj (e x) b )
-         cone-equ a b f se = slequ ? ? ? ?
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (equ (elem (e se) refl)) a) ]
-              ≈ Sets [ (λ se → proj (equ (elem (e se) refl)) b) o FMap (K Sets C lim) f ] ]
+         cequ :  (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) → (b : Obj C )  → sproduct (Obj C) (ΓObj s  Γ)
+         cequ se b = equ {_} {sproduct (Obj C) (ΓObj s Γ)}  {ΓObj s Γ b} {λ x → proj x b }  {λ x → proj x b} (elem (e se) refl)
+         cone-equ : (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
+              → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x →  FMap Γ (hom← s f) (proj (e x) a) ) (λ x → proj (e x) b )
+         cone-equ a b f se = elem se ( fe=ge0 (slequ se ( λ x → record { proj = λ i → proj ( e se ) i  } )  a b f ) )
+         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (cequ se b) a) ]
+              ≈ Sets [ (λ se → proj (cequ se b) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
          commute1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
-                 (Sets [ FMap Γ f o (λ se → proj (equ (elem (e se) refl)) a) ]) se
+                 (Sets [ FMap Γ f o (λ se → proj (cequ se b) a) ]) se
              ≡⟨⟩
                   FMap Γ f (proj (e se) a )
-             ≡⟨  fe=ge0 (cone-equ a b f se ) ⟩
+             ≡⟨  ≡cong ( λ g → FMap Γ g (proj (e se) a))  (sym ( hom-iso s  ) ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (proj (e se) a)
+             ≡⟨  fe=ge0 (cone-equ a b ( hom→ s f) se ) ⟩
                   proj (e se) b 
              ≡⟨⟩
-                  (Sets [ (λ se → proj (equ (elem (e se) refl)) b) o FMap (K Sets C lim) f ]) se
+                  (Sets [ (λ se → proj (cequ se b) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning