Mercurial > hg > Members > kono > Proof > category

changeset 576:9455768b05f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sproj approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 27 Apr 2017 20:54:16 +0900
parents 761df92aa225
children de530823f80b
files SetsCompleteness.agda
diffstat 1 files changed, 25 insertions(+), 99 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu Apr 27 10:51:29 2017 +0900
+++ b/SetsCompleteness.agda	Thu Apr 27 20:54:16 2017 +0900
@@ -47,13 +47,13 @@
           prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl
 
 
-record iproduct {a} (I : Set a)  ( Product : I → Set a ) : Set a where
+record sproduct {a} (I : Set a)  ( Product : I → Set a ) : Set a where
     field
        proj : ( i : I ) → Product i
 
-open iproduct
+open sproduct
 
-iproduct1 : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
+iproduct1 : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (sproduct I fi)
 iproduct1 I fi {q} qi x = record { proj = λ i → (qi i) x  }
 ipcx : {  c₂ : Level} → (I : Obj (Sets {  c₂})) (fi : I → Obj Sets ) {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 I fi qi x ≡ iproduct1 I fi qi' x
 ipcx I fi {q} {qi} {qi'} qi=qi x  = 
@@ -71,7 +71,7 @@
      → IProduct ( Sets  {  c₂} ) I
 SetsIProduct I fi = record {
        ai =  fi
-       ; iprod = iproduct I fi
+       ; iprod = sproduct I fi
        ; pi  = λ i prod  → proj prod i
        ; isIProduct = record {
               iproduct = iproduct1 I fi 
@@ -82,7 +82,7 @@
    } where
        pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj prod i) o iproduct1 I fi qi ] ≈ qi i ]
        pif=q {q} qi {i} = refl
-       ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ]
+       ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (sproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ]
        ip-uniqueness = refl
 
 
@@ -179,37 +179,19 @@
     {i j : Obj C } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
 ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f ) 
 
+sid :   { c₂  : Level}  { I :  Set  c₂ } → I → I
+sid x = x
 
-record slim  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I ) → sobj i → sobj j ) 
+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 (iproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
-   snmap : OC →  Set  c₂ 
-   snmap i = sobj i
-   ipp : {i j : OC } → (f : I → I ) → iproduct OC sobj
-   ipp {i} {j} f = equ ( slequ {i} {j} f )
+       sproj : (i : OC) → sobj i
+       slequ : { i j : OC } → ( f :  I → I ) →  sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
+   ipp : sproduct OC sobj
+   ipp = record { proj = sproj }
 
 open slim
 
-lemma-equ :   {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
-    {i j j' : Obj C } →　 ( f f' : I → I ) 
-    →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
-    →  proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {j'} f' ) i
-lemma-equ C I s Γ {i} {j} f f' se =   ≡cong ( λ p -> proj p i ) ( begin
-                 ipp se f 
-             ≡⟨⟩
-                 record { proj = λ i → proj (equ (slequ se f)) i }
-             ≡⟨ ≡cong ( λ p → record { proj =  proj p i })  (  ≡cong ( λ QIX → record { proj = QIX } ) (  
-                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  )  refl
-              ) )) ⟩
-                 record { proj = λ i → proj (equ (slequ se f')) i }
-             ≡⟨⟩
-                 ipp se f'  
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-
-
 open import HomReasoning
 open NTrans
 
@@ -217,83 +199,27 @@
 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 {
-               TMap = λ i →  λ se → proj ( ipp se {i} {i} (\x -> x) ) i
+               TMap = λ i →  λ se → proj ( ipp se ) i
              ; isNTrans = record { commute = commute1 }
       } where
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se  (\x -> x) ) a) ] ≈
-                Sets [ (λ se → proj ( ipp se  (\x -> x) ) 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 (ipp se) a) ] ≈
+                Sets [ (λ se → proj (ipp 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 ( ipp se  (\x -> x) ) a) ]) se
+                   (Sets [ FMap Γ f o (λ se₁ → proj (ipp se) a) ]) se
              ≡⟨⟩
-                   FMap Γ f (proj ( ipp se {a} {a} (\x -> x) ) a)
-             ≡⟨  ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (\x -> x) ) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {a} (\x -> x) ) a)
-             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ (\x -> x) (hom→ s f) se ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {b} (hom→ s f) ) a)
+                   FMap Γ f (proj (ipp se) a)
+             ≡⟨  ≡cong ( λ g → FMap Γ g (proj (ipp se) a))  (sym ( hom-iso s  ) ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (proj (ipp se) a)
+             ≡⟨  {!!}    ⟩
+                  ((Sets [ (λ x → ΓMap s Γ (hom→ s f) (proj x a)) o equ ]) (slequ se (hom→ s f)))
+
              ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
-                   proj (ipp se {a} {b} ( hom→ s f  )) b
+                  {!!}
              ≡⟨  {!!}    ⟩
-                   proj (ipp se {b} {b} (λ x → x)) b
+                   proj (ipp se) b
              ≡⟨⟩
-                  (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
+                  (Sets [ (λ se₁ → proj (ipp se) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
-
-
-
-SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
-    → Limit Sets C Γ
-SetsLimit { c₂} C I s Γ = record { 
-           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ)  
-         ; t0 = Cone C I s Γ 
-         ; isLimit = record {
-               limit  =  limit1 
-             ; t0f=t = λ {a t i } → refl
-             ; limit-uniqueness  =  λ {a} {t} {f} → uniquness1 {a} {t} {f}
-          }
-       }  where
-              limit2 :  (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → {i j : Obj C } →　 ( f : I → I ) 
-                    → ( x : a )  → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
-              limit2 a t f x =   ≡cong ( λ g → g x )   ( IsNTrans.commute ( isNTrans t  ) )
-              limit1 :  (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )
-              limit1 a t x = record {
-                   slequ = λ {i} {j} f → elem ( record { proj = λ i → TMap t i x }  ) ( limit2 a t f x  )
-                } 
-              uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)  )} 
-                     →  ( i j : Obj C  ) →
-                    ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) →  (f' : I → I ) →  (x : a ) 
-                     →  record { proj = λ i₁ → TMap t i₁ x }  ≡ equ (slequ (f x) f')
-              uniquness2 {a} {t} {f} i j cif=t f' x = begin
-                  record { proj = λ i → TMap t i x }
-                ≡⟨   ≡cong ( λ g → record { proj = λ i → g i  } ) (  extensionality Sets  ( λ i →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
-                  record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
-                ≡⟨⟩
-                  record { proj = λ i →   proj (ipp (f x) {i} {i} (\x -> x) ) i }
-                ≡⟨ ≡cong ( λ g →   record { proj = λ i' -> g i' } ) ( extensionality Sets  ( λ  i''  → ? lemma-equ C I s Γ ? ? (f x)))  ⟩
-                  record { proj = λ i →  proj (ipp (f x) {{!!}} {{!!}} f') i  }
-                ∎   where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-              uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)  )} →
-                    ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t  ≈ f ]
-              uniquness1 {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
-                  limit1 a t x
-                ≡⟨⟩
-                   record { slequ = λ {i} {j} f' → elem ( record { proj = λ i → TMap t i x }  ) ( limit2 a t f' x ) }
-                ≡⟨ ≡cong ( λ e → record { slequ =  λ {i} {j} f' → e i j f' x } ) (
-                        extensionality Sets  ( λ  i  →
-                           extensionality Sets  ( λ  j  →
-                               extensionality Sets  ( λ  f'  →
-                                   extensionality Sets  ( λ  x  → 
-                  elm-cong (  elem ( record { proj = λ i → TMap t i x }  ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' x ) )
-                           )))
-                     ) ⟩
-                   record { slequ = λ {i} {j} f' → slequ (f x ) f' }
-                ≡⟨⟩
-                  f x
-                ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-