Mercurial > hg > Members > kono > Proof > category

changeset 591:9676a75c3010

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
slid rewrite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 May 2017 16:46:54 +0900
parents 2c5d8c3c9086
children 0448a74c0a03 9367813d3f61
files SetsCompleteness.agda
diffstat 1 files changed, 22 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun May 14 13:53:26 2017 +0900
+++ b/SetsCompleteness.agda	Sun May 14 16:46:54 2017 +0900
@@ -174,20 +174,21 @@
     {i j : Obj C } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
 ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f ) 
 
-slid :   {  c₁  : Level}  { I :  Set  c₁ }  →   I → I
-slid x = x
+slid :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) → (x : Obj C)  →   I → I
+slid C I s x = hom→ s ( id1 C x )
 
 record slim  { c₂ }  { I OC :  Set  c₂ } 
                 ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I ) → sobj i → sobj j ) 
       :  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 :  {i : OC } → sproduct OC  sobj 
-   slprod {i} = equ ( slequ i i slid )
    slmap  :  { i j :  OC  }  → (f : I → I ) → sobj i → sobj j
    slmap f x = smap f x
+open slim
 
-open slim
+slprod :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
+    {i  : Obj C }  → (se : slim (ΓObj s Γ) (ΓMap s Γ)  )  → sproduct (Obj C)   (ΓObj s Γ)
+slprod C I s Γ {i} se = equ ( slequ se i i (slid C I s i ) )
 
 open import HomReasoning
 open NTrans
@@ -195,16 +196,12 @@
 llid :  {  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 Γ)  ) 
     → ( x : FObj Γ a )
-    → slmap se slid x ≡ x
+    → slmap se (slid C I s a ) x ≡ x
 llid C I s Γ a b f se x = begin
-        slmap se slid x 
-       ≡⟨  ≡cong ( λ g → slmap se g x )  (sym ( iso-hom s  ) ) ⟩
-        slmap se ((hom→ s (hom← s slid)) ) x 
+        slmap se (slid C I s a) x 
        ≡⟨⟩
-         FMap Γ (hom← s (hom→ s (hom← s slid))) x
+         FMap Γ (hom← s (slid C I s a)) x
        ≡⟨  ≡cong ( λ g → FMap Γ g  x )  (hom-iso s ) ⟩
-         FMap Γ (hom← s slid) x
-       ≡⟨ {!!} ⟩
          FMap Γ (id1 C a) x
        ≡⟨ ≡cong ( λ g →  g x ) ( IsFunctor.identity (isFunctor  Γ ) ) ⟩
          x
@@ -221,13 +218,13 @@
 
 lla :  {  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 Γ)  ) 
-    → proj ( equ ( slequ se a b f)) a ≡ proj (slprod se {a}) a 
+    → proj ( equ ( slequ se a b f)) a ≡ proj (slprod C I s Γ {a} se ) a 
 lla C I s Γ a b f se = begin
           proj ( equ ( slequ se a b f)) a 
        ≡⟨ fe=ge0 {!!} ⟩
-          proj ( equ ( slequ se a a slid)) a 
+          proj ( equ ( slequ se a a (slid C I s a))) a 
        ≡⟨⟩
-          proj (slprod se {a}) a
+          proj (slprod C I s Γ {a} se ) a
        ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -235,7 +232,7 @@
 
 llb :  {  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 Γ)  ) 
-    → proj ( equ ( slequ se a b f)) b ≡ proj (slprod se {b}) b 
+    → proj ( equ ( slequ se a b f)) b ≡ proj  (slprod C I s Γ {b} se ) b 
 llb C I s Γ a b f se = {!!}
 
 
@@ -243,25 +240,25 @@
     → NTrans C Sets (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)))  Γ
 Cone {c₁} C I s  Γ =  record {
                TMap = λ i →  λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s  Γ)}  {FObj Γ i}
-                     {λ x → proj x i} {λ x → proj x i} (elem (slprod se) refl )) i
+                     {λ x → proj x i} {λ x → proj x i} (elem  (slprod C I s Γ {i} se ) refl )) i
              ; isNTrans = record { commute = commute1 }
       } where
-         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 : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj  (slprod C I s Γ {a} se ) a) ]
+              ≈ Sets [ (λ se → proj  (slprod C I s Γ {b} 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}) a) ]) se
+                 (Sets [ FMap Γ f o (λ se → proj  (slprod C I s Γ {a} se ) 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}) a)
+                  FMap Γ f (proj  (slprod C I s Γ {a} se ) a )
+             ≡⟨  ≡cong ( λ g → FMap Γ g (proj  (slprod C I s Γ {a} se ) a))  (sym ( hom-iso s  ) ) ⟩
+                  FMap Γ  (hom← s ( hom→ s f))  (proj  (slprod C I s Γ {a} se ) a)
              ≡⟨  ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g ) (sym (lla C I s Γ a b ( hom→ s f)  se ) ) ⟩
                   FMap Γ  (hom← s ( hom→ s f))  (proj (equ ( slequ se a b ( hom→ s f))) a)
              ≡⟨  fe=ge0 (slequ se a b ( hom→ s f) ) ⟩
                   proj (equ (slequ se a b ( hom→ s f))) b
              ≡⟨  llb C I s Γ a b ( hom→ s f)  se ⟩
-                  proj (slprod se {b}) b 
+                  proj  (slprod C I s Γ {b} se ) b 
              ≡⟨⟩
-                  (Sets [ (λ se → proj (slprod se {b}) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
+                  (Sets [ (λ se → proj  (slprod C I s Γ {b} se ) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning