Mercurial > hg > Members > kono > Proof > category

changeset 593:a158ebb391f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 May 2017 19:53:58 +0900
parents 0448a74c0a03
children db76b73b526c
files SetsCompleteness.agda
diffstat 1 files changed, 40 insertions(+), 121 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon May 15 18:09:33 2017 +0900
+++ b/SetsCompleteness.agda	Sun May 21 19:53:58 2017 +0900
@@ -180,134 +180,36 @@
                 ( 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 )
+       slproj : ( i : OC ) → sobj i 
+       slequ : (i j : OC) (f :  I → I  ) → sequ OC (sobj j) (λ x →  smap f (slproj i) ) (λ x → slproj j )
+   slprod : sproduct OC  sobj
+   slprod = record { proj = slproj }
    slmap  :  { i j :  OC  }  → (f : I → I ) → sobj i → sobj j
    slmap f x = smap f x
 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
-                  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 c : Obj C) (f g : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ)  ) 
-    → ( x : FObj Γ a )
-    → slmap se {a} {c} ( λ y → f ( g y )) x ≡ slmap se {b} {c} f ( ( slmap se {a} {b} g ) x )
-lldistr C I s Γ a b c f g se x =   begin
-          slmap se {a} {c} ( λ y → f ( g y )) x
-       ≡⟨⟩
-           FMap Γ (hom← s (λ y → f (g y)))  x
-       ≡⟨ ?  ⟩
-           FMap Γ (hom← s (λ y → f ( hom→ s ( hom← s  g) y )))  x
-       ≡⟨ {!!} ⟩
-           FMap Γ  (C [ hom← s f o hom← s g ]) x
-       ≡⟨  ≡cong ( λ g →  g x ) ( IsFunctor.distr (isFunctor  Γ ) )  ⟩
-           (Sets [ FMap Γ (hom← s f) o FMap Γ (hom← s g ) ]) x
-       ≡⟨⟩
-          slmap se {b} {c} f ( ( slmap se {a} {b} g ) x )
-       ∎  where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-
-
-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 (equ (slequ se i j f)) i ≡ proj (equ (slequ se i' j' f' )) i
-lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se =   ≡cong ( λ p -> proj p i ) ( begin
-                 equ (slequ se i j f )
-             ≡⟨⟩
-                 record { proj = λ x → proj (equ (slequ se i j 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 i' j' f')) x }
-             ≡⟨⟩
-                 equ (slequ  se i' j' f' )
+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 ( slprod se ) 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} {f} =   extensionality Sets  ( λ  se  →  begin  
+                  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)
+             ≡⟨  fe=ge0 (slequ se a b ( hom→ s f) ) ⟩
+                  proj (slprod se) b
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
-llcomm :  {  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 ≡  slmap se f (proj (slprod C I s Γ {a} se ) a )
-llcomm C I s Γ a b f se  =  begin
-          proj ( equ ( slequ se a b f)) a
-       ≡⟨ {!!} ⟩
-          slmap se f (proj (equ ( slequ se a a (slid C I s a))) a )
-       ≡⟨⟩
-          slmap se f (proj (slprod C I s Γ {a} se ) a )
-       ∎  where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-
-
-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 
-       ≡⟨ {!!} ⟩
-          proj ( equ ( slequ se a a (slid C I s a))) a 
-       ∎  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 = {!!}
-
-
-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 (slprod C I s Γ {i} se ) 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} {f} =   extensionality Sets  ( λ  se  →  begin  
-                 (Sets [ FMap Γ f o (λ se → proj  (slprod C I s Γ {a} se ) 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 
-             ≡⟨⟩
-                  (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
-
-
-
 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 { 
@@ -315,11 +217,28 @@
          ; t0 = Cone C I s Γ 
          ; isLimit = record {
                limit  = limit1
-             ; t0f=t = λ {a t i } → {!!}
-             ; limit-uniqueness  =  λ {a t i }  → {!!}
+             ; t0f=t = λ {a t i } → refl
+             ; limit-uniqueness  =  λ {a t f }  → limit-uniqueness {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 )))    }
+          limit1 a t = λ x →  record {
+               slequ =  λ i j f → elem {!!} ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ))
+               ; slproj =  λ i → ( TMap t i ) x
+             }
+          limit-uniqueness :  {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 ]
+          limit-uniqueness {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
+                  limit1 a t x
+             ≡⟨ {!!} ⟩
+                  f x
+             ∎  ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+
+                 
+
+
+
+
+