Mercurial > hg > Members > kono > Proof > category

changeset 605:af321e38ecee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
another snat-cong approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Jun 2017 12:53:54 +0900
parents 75112154faf0
children 92eb707498c7
files SetsCompleteness.agda system-t.agda
diffstat 2 files changed, 64 insertions(+), 71 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Jun 05 21:42:21 2017 +0900
+++ b/SetsCompleteness.agda	Thu Jun 08 12:53:54 2017 +0900
@@ -1,11 +1,9 @@
-
-open import Category -- https://github.com/konn/category-agda
+open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 open import Category.Sets renaming ( _o_ to _*_ )
 
 module SetsCompleteness where
 
-
 open import cat-utility
 open import Relation.Binary.Core
 open import Function
@@ -13,7 +11,7 @@
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-≡cong = Relation.Binary.PropositionalEquality.cong
+≡cong = Relation.Binary.PropositionalEquality.cong 
 
 lemma1 :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} {f g : Hom Sets a b} →
    Sets [ f ≈ g ] → (x : a ) → f x  ≡ g x
@@ -23,18 +21,18 @@
   constructor _,_
   field
     proj₁ : A
-    proj₂ : B
+    proj₂ : B 
 
 open Σ public
 
 
 SetsProduct :  {  c₂ : Level} → CreateProduct ( Sets  {  c₂} )
-SetsProduct { c₂ } = record {
+SetsProduct { c₂ } = record { 
          product =  λ a b →    Σ a  b
        ; π1 = λ a b → λ ab → (proj₁ ab)
        ; π2 = λ a b → λ ab → (proj₂ ab)
        ; isProduct =  λ a b → record {
-              _×_  = λ f g  x →   record { proj₁ = f  x ;  proj₂ =  g  x }     -- ( f x ,  g x )
+              _×_  = λ f g  x →   record { proj₁ = f  x ;  proj₂ =  g  x }     -- ( f x ,  g x ) 
               ; π1fxg=f = refl
               ; π2fxg=g  = refl
               ; uniqueness = refl
@@ -53,7 +51,7 @@
 
 open iproduct
 
-SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
+SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) 
      → IProduct ( Sets  {  c₂} ) I
 SetsIProduct I fi = record {
        ai =  fi
@@ -73,21 +71,21 @@
        ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
        ip-uniqueness = refl
        ipcx : {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x
-       ipcx {q} {qi} {qi'} qi=qi x  =
+       ipcx {q} {qi} {qi'} qi=qi x  = 
               begin
                 record { pi1 = λ i → (qi i) x  }
              ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x )  (qi=qi i)  )) ⟩
                 record { pi1 = λ i → (qi' i) x  }
              ∎  where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+                  open  import  Relation.Binary.PropositionalEquality 
+                  open ≡-Reasoning 
        ip-cong  : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1  qi' ]
        ip-cong {q} {qi} {qi'} qi=qi  = extensionality Sets ( ipcx qi=qi )
 
 
         --
         --         e             f
-        --    c  -------→ a ---------→ b        f ( f'
+        --    c  -------→ a ---------→ b        f ( f' 
         --    ^        .     ---------→
         --    |      .            g
         --    |k   .
@@ -100,9 +98,9 @@
     elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
 
 equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b  f g ) →  a
-equ  (elem x eq)  = x
+equ  (elem x eq)  = x 
 
-fe=ge0  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →
+fe=ge0  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →  
      (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
 fe=ge0 (elem x eq )  =  eq
 
@@ -115,18 +113,18 @@
 --          ; equalizer = λ e → equ e
 
 SetsIsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g
-SetsIsEqualizer {c₂} a b f g = record {
+SetsIsEqualizer {c₂} a b f g = record { 
                fe=ge  = fe=ge
              ; k = k
              ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
              ; uniqueness  = uniqueness
        } where
            fe=ge  :  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
-           fe=ge  =  extensionality Sets (fe=ge0 )
+           fe=ge  =  extensionality Sets (fe=ge0 ) 
            k :  {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
            k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
            ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
-           ek=h {d} {h} {eq} = refl
+           ek=h {d} {h} {eq} = refl 
            injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
            injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
            elm-cong :   (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
@@ -153,65 +151,50 @@
 record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-     hom→ : {i j : Obj C } →    Hom C i j →  I →  I
-     hom← : {i j : Obj C } →  ( f : I  →  I ) →  Hom C i j
-     hom-iso : {i j : Obj C } →  { f : Hom C i j } →   hom← ( hom→ f )  ≡ f
-     -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
+     hom→ : {i j : Obj C } →    Hom C i j →  I  
+     hom← : {i j : Obj C } →  ( f : I ) →  Hom C i j 
+     hom-iso : {i j : Obj C } →  { f : Hom C i j } →   hom← ( hom→ f )  ≡ f 
 
-open Small
+open Small 
 
-ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
+ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
    (i : Obj C ) →　 Set c₁
 ΓObj s  Γ i = FObj Γ i
 
-ΓMap :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
-    {i j : Obj C } →　 ( f : I  →  I ) →  ΓObj s Γ i → ΓObj  s Γ j
-ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f )
+ΓMap :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
+    {i j : Obj C } →　 ( f : I ) →  ΓObj s Γ i → ΓObj  s Γ j 
+ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f ) 
 
-record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ )
-     ( smap : { i j :  OC  }  → (f : I  →  I )→  sobj i → sobj j ) : Set  c₂ where
-   field
-       snmap : ( i : OC ) → sobj i
-       sncommute : { i j : OC } → ( f :  I  →  I ) →  ( m :  ( i : OC ) → sobj i)  →  smap f ( m i )  ≡ m j
+record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) 
+     ( smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j ) : Set  c₂ where
+   field 
+       snmap : ( i : OC ) → sobj i 
+       sncommute : { i j : OC } → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
+   smap0 :  { i j :  OC  }  → (f : I ) →  sobj i → sobj j
+   smap0 {i} {j} f x =  smap f x
 
 open snat
 
-
-≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C )
+≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C ) 
     →  a  ≡  a'
     →  b  ≡  b'
     →  f a b  ≡  f a' b'
 ≡cong2 _ refl refl = refl
 
-
-snat-cong :  { c : Level }  { I OC :  Set  c }  ( SObj :  OC →  Set  c  ) ( SMap : { i j :  OC  }  → (f : I  →  I )→  SObj i → SObj j)
-         { s t :  snat SObj SMap   }
-     → (( i : OC ) → snmap s i ≡  snmap t i )
+snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
+         ( s t :  snat SObj SMap   )
+     → ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i) )
+     → ( ( λ {i} {j} f →  smap0 s f ( snmap s i )  ≡ snmap s j ) ≡ ( λ {i} {j} f → smap0 t f ( snmap t i )  ≡ snmap t j ) )
      → s ≡ t
-snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  =  begin
-     record { snmap = λ i →  snmap s i ; sncommute  = λ {i} {j} f → sncommute s f  }
- ≡⟨
-    ≡cong2 ( λ x y →
-      record { snmap = λ i → x i  ; sncommute  = λ {i} {j} f m →  y x i j f m } )  (  extensionality Sets  ( λ  i  →  (eq1 i) ) )
-           ( extensionality Sets  ( λ  x  →
-           ( extensionality Sets  ( λ  i  →
-             ( extensionality Sets  ( λ  j  →
-               ( extensionality Sets  ( λ  f  →  
-                 ( extensionality Sets  ( λ  m  →  irr (sncommute s f m) (sncommute t f m)
-             ))))))))))
-  ⟩
-     record { snmap = λ i →  snmap t i ; sncommute  = λ {i} {j} f → sncommute t f  }
-             ∎   where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+snat-cong {_} {I} {OC} {SO} {SM} s t eq1 eq2 =  {!!}
 
 open import HomReasoning
 open NTrans
 
-Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
+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 (snat  (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
 Cone C I s  Γ  =  record {
-               TMap = λ i →  λ sn →  snmap sn i
+               TMap = λ i →  λ sn →  snmap sn i 
              ; isNTrans = record { commute = comm1 }
       } where
     comm1 :  {a b : Obj C} {f : Hom C a b} →
@@ -222,18 +205,18 @@
              ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( hom-iso s  )) ⟩
                  FMap Γ ( hom← s ( hom→ s f))  (snmap sn  a )
              ≡⟨⟩
-                 ΓMap s Γ (hom→ s f) (snmap sn a )
-             ≡⟨ sncommute sn (hom→ s  f) (snmap sn) ⟩
+                 ΓMap s Γ (hom→ s f) (snmap sn a ) 
+             ≡⟨ sncommute sn (hom→ s  f) ⟩
                  snmap sn b
              ∎  ) 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₁} ) )
+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 =  snat  (ΓObj s Γ) (ΓMap s Γ)
+SetsLimit { c₂} C I s Γ = record { 
+           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
          ; t0 = Cone C I s Γ
          ; isLimit = record {
                limit  = limit1
@@ -241,19 +224,15 @@
              ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
           }
        }  where
-          a0 : Obj Sets
-          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ)
-          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I →  I ) ( m : (i :  Obj C ) → ΓObj s Γ i )
-             → ΓMap s Γ f (m i) ≡ m j
-          comm2 {a} {x} t f m =  {!!}
-          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
+          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) 
+             → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
+          comm2 {a} {x} t f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
+          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
-              sncommute = λ f m → comm2 {a} {x} t f m }
+              sncommute = λ f → comm2 t f }
           t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ]
           t0f=t {a} {t} {i} =  extensionality Sets  ( λ  x  →  begin
                  ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x
-             -- ≡⟨⟩
-                 -- snmap ( record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ {i j} f → comm2 {a} {x} {i} {j} t f }  ) i
              ≡⟨⟩
                  TMap t i x
              ∎  ) where
@@ -264,8 +243,11 @@
           limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
                   limit1 a t x
              ≡⟨⟩
-                  record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f m → comm2 {a} {x} t f m }
-             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) (eq1 x)   ⟩
+                  record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }
+             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) 
+                (
+                   {!!}
+                )⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
              ≡⟨⟩
                   f x
--- a/system-t.agda	Mon Jun 05 21:42:21 2017 +0900
+++ b/system-t.agda	Thu Jun 08 12:53:54 2017 +0900
@@ -79,6 +79,17 @@
 sum : Int → Int → Int
 sum x y = R y ( λ z → λ w → S z ) x
 
+sum2 : Int → Int → Int
+sum2 zero x = x
+sum2 (S x) y = S ( sum2 x y )
+
+cong1 : { x y :  Int } -> ( f : Int -> Int ) ->  x ≡ y -> f x ≡ f y 
+cong1 {x} {.x} f refl = refl
+
+lemma1 : ( x y : Int ) → sum x y  ≡ sum2 x y
+lemma1 zero y  = refl
+lemma1 (S x) y = cong1 ( λ z -> S z ) ( lemma1 x y )
+
 mul : Int → Int → Int
 mul x y = R zero ( λ z → λ w → sum y z ) x