Mercurial > hg > Members > kono > Proof > category

changeset 540:2373c11a93f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Mar 2017 08:49:10 +0900
parents 9a657775d81e
children 505962017fd1
files SetsCompleteness.agda
diffstat 1 files changed, 28 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 31 08:11:46 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 31 08:49:10 2017 +0900
@@ -152,9 +152,9 @@
 record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-     shom→ : {i j : Obj C } →    Hom C i j →  I  
-     shom← : {i j : Obj C } →  ( f : I ) →  Hom C i j 
-     shom-iso : {i j : Obj C } →  { f : Hom C i j } →   shom← ( shom→ 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 
      -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
 
 open Small 
@@ -165,7 +165,7 @@
 
 Γ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 Γ ( shom← s f ) 
+Γ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 )→  sobj i → sobj j ) : Set  c₂ where
@@ -190,11 +190,11 @@
         Sets [ (λ sn →  (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
     comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
                  FMap Γ f  (snmap sn  a )
-             ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( shom-iso s  )) ⟩
-                 FMap Γ ( shom← s ( shom→ s f))  (snmap sn  a )
+             ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( hom-iso s  )) ⟩
+                 FMap Γ ( hom← s ( hom→ s f))  (snmap sn  a )
              ≡⟨⟩
-                 ΓMap s Γ (shom→ s f) (snmap sn a ) 
-             ≡⟨ sncommute sn (shom→ s  f) ⟩
+                 ΓMap s Γ (hom→ s f) (snmap sn a ) 
+             ≡⟨ sncommute sn (hom→ s  f) ⟩
                  snmap sn b
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
@@ -222,10 +222,28 @@
           limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
               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 = {!!}
+          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
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
           limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (Γ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 = {!!}
+          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 }
+             ≡⟨ {!!} ⟩
+                  record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ f → ? }
+             ≡⟨⟩
+                  f x
+             ∎  ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning