Mercurial > hg > Members > kono > Proof > category

changeset 586:c78df4c0453c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 11 May 2017 17:06:27 +0900
parents 59c3de1c4043
children d3bea3ac919e
files SetsCompleteness.agda
diffstat 1 files changed, 16 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu May 11 15:58:34 2017 +0900
+++ b/SetsCompleteness.agda	Thu May 11 17:06:27 2017 +0900
@@ -188,6 +188,16 @@
 open import HomReasoning
 open NTrans
 
+cequ :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
+    → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)) (sproduct (Obj C) (ΓObj s  Γ) ))   (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) → (b : Obj C )  
+    → sproduct (Obj C) (ΓObj s  Γ)
+cequ C I s Γ e 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 :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
+    → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  ) (sproduct (Obj C) (ΓObj s  Γ)  )   )
+    →  (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 C I s Γ e a b f se = elem se ( fe=ge0 (slequ se ( λ x → record { proj = λ i → proj ( e se ) i  } )  a b f ) )
+
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
     → ( e : Hom Sets ( slim (ΓObj s Γ) (ΓMap s Γ)  ) (sproduct (Obj C) (ΓObj s  Γ)  ) )
     → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)))  Γ
@@ -196,23 +206,18 @@
                      {λ x → proj x i} {λ x → proj x i} (elem (e se ) refl )) i
              ; isNTrans = record { commute = commute1 }
       } where
-         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 : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (cequ C I s Γ e se b) a) ]
+              ≈ Sets [ (λ se → proj (cequ C I s Γ e 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 (cequ se b) a) ]) se
+                 (Sets [ FMap Γ f o (λ se → proj (cequ C I s Γ e se b) a) ]) se
              ≡⟨⟩
                   FMap Γ f (proj (e se) a )
              ≡⟨  ≡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 ) ⟩
+             ≡⟨  fe=ge0 (cone-equ  C I s Γ e a b ( hom→ s f) se ) ⟩
                   proj (e se) b 
              ≡⟨⟩
-                  (Sets [ (λ se → proj (cequ se b) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
+                  (Sets [ (λ se → proj (cequ C I s Γ e se b) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -234,5 +239,5 @@
              → ΓMap s Γ f (proj p i) ≡ proj p j
           comm2  e {i} {j} f p = {!!}
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
-          limit1 a t = λ x →  record { slequ = λ e i j f →　elem i {!!}
+          limit1 a t = λ x →  record { slequ = λ e i j f → ?
                ; slprod = record { proj = λ i → TMap t i x } }