Mercurial > hg > Members > kono > Proof > category

changeset 596:9367813d3f61

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lemma-equ retry
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 May 2017 10:39:18 +0900
parents 9676a75c3010
children b281e8352158
files SetsCompleteness.agda
diffstat 1 files changed, 116 insertions(+), 75 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun May 14 16:46:54 2017 +0900
+++ b/SetsCompleteness.agda	Tue May 23 10:39:18 2017 +0900
@@ -1,11 +1,9 @@
-
 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
@@ -88,12 +86,12 @@
 
         --
         --         e             f
-        --    c  -------→ a ---------→ b        f ( f' 
-        --    ^        .     ---------→
+        --    c  -------→ a ---------→ b        
+        --    ^        .    ---------→
         --    |      .            g
         --    |k   .
         --    |  . h
-        --y : d
+        --    d
 
         -- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda
 
@@ -161,7 +159,6 @@
      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 
-     iso-hom : {i j : Obj C } →  { f : I → I } →   hom→ ( hom← {i} {j} f )  ≡ f 
      -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
 
 open Small 
@@ -177,106 +174,150 @@
 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 ) 
+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 )
-   slmap  :  { i j :  OC  }  → (f : I → I ) → sobj i → sobj j
-   slmap f x = smap f x
+       slequ : { i j : OC } → ( f :  I → I ) →  sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) ( λ x → proj x j )
+   slobj : OC →  Set  c₂ 
+   slobj i = sobj i
+   slmap : {i j : OC } →  (f : I → I ) → sobj i → sobj j
+   slmap f = smap f 
+   ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj
+   ipp {i} {j} f = equ ( slequ {i} {j} f )
+
 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
-
-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 C I s a ) x ≡ x
-llid C I s Γ a b f se x = begin
-        slmap se (slid C I s a) x 
-       ≡⟨⟩
-         FMap Γ (hom← s (slid C I s a)) x
-       ≡⟨  ≡cong ( λ g → FMap Γ g  x )  (hom-iso s ) ⟩
-         FMap Γ (id1 C a) x
-       ≡⟨ ≡cong ( λ g →  g x ) ( IsFunctor.identity (isFunctor  Γ ) ) ⟩
-         x
-       ∎  where
+smap-id :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
+   ( se : slim  (ΓObj s Γ) (ΓMap s Γ) ) → (i : Obj C )  → (x : FObj Γ i ) → slmap se (slid C I s i) x ≡ x
+smap-id C I s Γ se i x =  begin
+             slmap se (slid C I s i) x
+          ≡⟨⟩
+             slmap se ( hom→ s (id1 C i)) x
+          ≡⟨⟩
+             FMap Γ (hom← s (hom→ s (id1 C i))) x
+          ≡⟨ ≡cong ( λ ii →  FMap Γ ii x ) (hom-iso s) ⟩
+             FMap Γ (id1 C i) x
+          ≡⟨ ≡cong ( λ f → f x ) (IsFunctor.identity ( isFunctor Γ) ) ⟩
+             x
+          ∎   where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
 
-lldistr :  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
-    →  (a b : Obj C) (f g : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
-    → ( x : FObj Γ a )
-    → slmap se ( λ y → f ( g y )) x ≡ slmap se f ( ( slmap se g ) x )
-lldistr C I s Γ a b f g se x =  {!!}
+product-to :    { c₂ : Level }  { I OC :  Set  c₂ } { sobj :  OC →  Set  c₂ } 
+      →  Hom Sets (sproduct OC sobj)  (sproduct OC sobj)
+product-to x =  record { proj = proj x }
+
+lemma-equ' :   {  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 } 
+    →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
+    →  proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {i} (slid C I s i) ) i
+lemma-equ' C I s Γ {i} {j} {f} se =   
+     fe=ge0 ?
 
-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 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 C I s a))) a 
-       ≡⟨⟩
-          proj (slprod C I s Γ {a} se ) a
-       ∎  where
+lemma-equ :   {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
+    {i j i' 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} {i'} {j'} {f} {f'} se =   ≡cong ( λ p → proj p i ) ( begin
+                 ipp se {i} {j} f 
+             ≡⟨⟩
+                 record { proj = λ x → proj (equ (slequ se f)) x }
+             ≡⟨ ≡cong ( λ p → record { proj =  proj p i })  (  ≡cong ( λ QIX → record { proj = QIX } ) (  
+                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  ) refl
+              ) )) ⟩
+                 record { proj = λ x → proj (equ (slequ se f')) x }
+             ≡⟨⟩
+                 ipp se {i'} {j'} f'  
+             ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
 
-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 C I s Γ {b} se ) b 
-llb C I s Γ a b f se = {!!}
+open import HomReasoning
+open NTrans
 
 
 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₁} 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 C I s Γ {i} se ) refl )) i
+    → 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
              ; isNTrans = record { commute = commute1 }
       } where
-         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 : 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} {f} =   extensionality Sets  ( λ  se  →  begin  
-                 (Sets [ FMap Γ f o (λ se → proj  (slprod C I s Γ {a} se ) a) ]) se
+                   (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se  (λ x → x) ) a) ]) se
              ≡⟨⟩
-                  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 C I s Γ {b} se ) b 
+                   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 Γ   se ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {b} (hom→ s f) ) a)
+             ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
+                   proj (ipp se {a} {b} ( hom→ s f  )) b
+             ≡⟨ sym ( lemma-equ C I s Γ se ) ⟩
+                   proj (ipp se {b} {b} (λ x → x)) b
              ≡⟨⟩
-                  (Sets [ (λ se → proj  (slprod C I s Γ {b} se ) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ)  )) f ]) se
+                  (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) 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 Γ) 
+           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ)  
          ; t0 = Cone C I s Γ 
          ; isLimit = record {
-               limit  = limit1
-             ; t0f=t = λ {a t i } → {!!}
-             ; limit-uniqueness  =  λ {a t i }  → {!!}
+               limit  =  limit1 
+             ; t0f=t = λ {a t i } → refl
+             ; limit-uniqueness  =  λ {a} {t} {f} → uniquness1 {a} {t} {f}
           }
        }  where
-          --    ( e : Obj C  → sproduct (Obj C) sobj  )
-          --    sequ (Obj C) (ΓObj s Γ j) (λ x₁ → ΓMap s Γ f (proj (e x₁) i)) (λ x₁ → proj (e x₁) j)
-          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 = λ i j f →  elem (record { proj = λ i → TMap t i x   }) ( ≡cong ( λ g → g x)  (IsNTrans.commute (isNTrans t )))    }
+              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
+