Mercurial > hg > Members > kono > Proof > category

changeset 589:6584db867bd0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 May 2017 09:55:10 +0900
parents 11b5eeb4a9e7
children 2c5d8c3c9086
files SetsCompleteness.agda
diffstat 1 files changed, 13 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri May 12 13:45:31 2017 +0900
+++ b/SetsCompleteness.agda	Sun May 14 09:55:10 2017 +0900
@@ -181,7 +181,8 @@
       :  Set   c₂  where
    field 
        slequ : (i j : OC) (f :  I → I  ) → sequ (sproduct OC sobj) (sobj j) (λ x →  smap f (proj x i) ) (λ x → proj x j )
-       slprod :  sproduct OC  sobj 
+   slprod :  {i : OC } → sproduct OC  sobj 
+   slprod {i} = equ ( slequ i i slid )
 
 open slim
 
@@ -190,9 +191,14 @@
 
 cone-equ :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
     →  (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 (slprod x) a) ) (λ x → proj (slprod x) b )
+    → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x →  FMap Γ (hom← s f) (proj (slprod x {a}) a) ) (λ x → proj (slprod x {b}) b )
 cone-equ C I s Γ a b f se = elem se {!!} -- (( fe=ge0 (slequ se  a b f  )) )
 
+cone-equ' :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
+    →  (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
+    →    FMap Γ (hom← s f) (proj (equ (slequ se a b f )) a) ≡  proj (equ (slequ se a b f)) b 
+cone-equ' C I s Γ a b f se  = fe=ge0 (slequ se  a b f ) 
+
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
     → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)))  Γ
 Cone C I s  Γ =  record {
@@ -203,15 +209,15 @@
          commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod se) a) ]
               ≈ Sets [ (λ se → proj (slprod se) 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 (slprod se) a) ]) se
+                 (Sets [ FMap Γ f o (λ se → proj (slprod se {a}) a) ]) se
              ≡⟨⟩
                   FMap Γ f (proj (slprod se) a )
              ≡⟨  ≡cong ( λ g → FMap Γ g (proj (slprod se) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj (slprod se) a)
+                   FMap Γ  (hom← s ( hom→ s f))  (proj (slprod se {a}) a)
              ≡⟨  fe=ge0 (cone-equ  C I s Γ a b ( hom→ s f) se ) ⟩
-                  proj (slprod se) b 
+                  proj (slprod se {b}) b 
              ≡⟨⟩
-                  (Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
+                  (Sets [ (λ se → proj (slprod se {b}) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -237,6 +243,5 @@
                       ≈⟨ car  (nat t)  ⟩
                          (λ x₁ → proj x₁ j) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x)
                       ∎ 
-                    ) x
-               ; slprod = record { proj = λ i → TMap t i x } } 
+                    ) x }
                         where open ≈-Reasoning (Sets { c₂})