Mercurial > hg > Members > kono > Proof > category

changeset 606:92eb707498c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for new agda Set Completeness unfinnished
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Jun 2017 19:26:12 +0900
parents af321e38ecee
children caab94e897e6
files HomReasoning.agda SetsCompleteness.agda list-nat.agda
diffstat 3 files changed, 54 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Thu Jun 08 12:53:54 2017 +0900
+++ b/HomReasoning.agda	Thu Jun 08 19:26:12 2017 +0900
@@ -130,7 +130,7 @@
       →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
   nat1 η f =  IsNTrans.commute ( isNTrans η  )
 
-  infixr  2 _∎
+  infix  3 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
   infixr 2 _≈↑⟨_⟩_ 
   infix  1 begin_
@@ -168,9 +168,8 @@
                  ( f : Hom A a b )
                       →  A [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) 
-  let open ≈-Reasoning (c) in 
-     begin  
-          c [ Id {_} {_} {_} {c} b o g ]
+  let open ≈-Reasoning (c) in begin  
+          c [ ( Id {_} {_} {_} {c} b ) o g ]
      ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
           g
      ∎
--- a/SetsCompleteness.agda	Thu Jun 08 12:53:54 2017 +0900
+++ b/SetsCompleteness.agda	Thu Jun 08 19:26:12 2017 +0900
@@ -1,4 +1,4 @@
-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 _*_ )
 
@@ -11,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
@@ -21,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
@@ -51,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
@@ -71,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   .
@@ -98,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
 
@@ -113,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
@@ -151,50 +151,52 @@
 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  
-     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 
+     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 ) →  Γ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₂ ) 
+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
+   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
 
+open import Relation.Binary.HeterogeneousEquality as HE renaming ( sym to sym' )
+
 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 ) )
+     → ( ( λ 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 eq2 =  {!!}
+snat-cong s t refl refl = {!!}
 
 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} →
@@ -205,18 +207,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) ⟩
+                 ΓMap s Γ (hom→ s f) (snmap sn a )
+             ≡⟨ sncommute sn a b  (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
@@ -224,12 +226,12 @@
              ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
           }
        }  where
-          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) 
+          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 : 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 → comm2 t f }
+              sncommute = λ i j 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
@@ -243,12 +245,9 @@
           limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
                   limit1 a t 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 ) }
+                  record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
+             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq2 x )  ⟩
+                  record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j f' → sncommute (f x ) i j f'  }
              ≡⟨⟩
                   f x
              ∎  ) where
@@ -256,3 +255,6 @@
                   open ≡-Reasoning
                   eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
                   eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
+                  eq2 : ( x : a) → (λ i j f₁ → smap0 (limit1 a t x) f₁ (snmap (limit1 a t x) i) ≡ snmap (limit1 a t x) j)
+                        ≡ (λ i j  f₁ → smap0 (f x) f₁ (snmap (f x) i) ≡ snmap (f x) j)
+                  eq2 x = {!!}
--- a/list-nat.agda	Thu Jun 08 12:53:54 2017 +0900
+++ b/list-nat.agda	Thu Jun 08 19:26:12 2017 +0900
@@ -72,7 +72,7 @@
 
 module ==-Reasoning  (A : Set  ) where
 
-  infixr  2 _∎
+  infix  3 _∎
   infixr 2 _==⟨_⟩_ _==⟨⟩_
   infix  1 begin_
 
@@ -100,6 +100,7 @@
 lemma11 A x =  let open ==-Reasoning A in
      begin x ∎
       
+
 ++-assoc :  (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
 ++-assoc A [] ys zs = let open ==-Reasoning A in
   begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)