Mercurial > hg > Members > kono > Proof > category

changeset 535:5d7f8921bac0

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 Thu, 30 Mar 2017 17:08:16 +0900
parents a90889cc2988
children 09beac05a0fb
files SetsCompleteness.agda
diffstat 1 files changed, 42 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Wed Mar 29 14:24:09 2017 +0900
+++ b/SetsCompleteness.agda	Thu Mar 30 17:08:16 2017 +0900
@@ -1,7 +1,7 @@
 
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
-open import Category.Sets
+open import Category.Sets renaming ( _o_ to _*_ )
 
 module SetsCompleteness where
 
@@ -152,12 +152,29 @@
      small→ : Obj C → I
      small← : I → Obj C
      small-iso : { x : Obj C  } → Hom C (small← ( small→ x ))  x
+     small-≡   : { x : Obj C  } →  (small← ( small→ x )) ≡ x
      shom→ : {i j : Obj C  } →    Hom C i j →  I → I 
      shom← : {i j : I } →  ( f : I → I ) →  Hom C ( small←  i  ) (  small←  j )
      shom-iso : {i j : I } →  ( f : Hom C ( small←  i  ) (  small←  j ) ) →  C [ shom← ( shom→ f )  ≈ f ]
 
 open Small 
 
+≡subst : {c : Level } { x y : Set c } { f :  Set c → Set c } → ( x ≡ y ) → f x ≡ f y 
+≡subst {c} {x} {.x} {f} refl =  ≡cong ( λ x → f x ) refl
+
+small-hom-iso : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )  { x y : Obj C  }  → 
+    (s : Small C I ) → Hom C (small← s ( small→ s x )) y  ≡ Hom C x y
+small-hom-iso C I {x} {y} s = ≡cong ( λ x → Hom C x y ) ( small-≡ s )
+
+small-hom-iso' : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )  { x y : Obj C  }  → 
+    (s : Small C I ) → Hom C (small← s ( small→ s x )) y  →  Hom C x y
+small-hom-iso' C I {x} {y} s f = {!!}
+
+iid :   {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ }  {I :  Set  c₁} ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) ){i : Obj C } → 
+     Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
+iid  s Γ = FMap Γ ( small-iso s ) 
+
+
 ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
    (i : I ) →　 Set c₁
 ΓObj s  Γ i = FObj Γ (small← s i )
@@ -175,25 +192,36 @@
 open snat
 
 open import HomReasoning
+
 open NTrans
 
-SetsNat : {  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 Γ) ) ) Γ
-SetsNat C I s  Γ  =  record {
-               TMap = λ i →  λ sn →  iid ( snmap sn (small→ s i )  )
+Cone C I s  Γ  =  record {
+               TMap = λ i →  λ sn →  iid s Γ ( snmap sn (small→ s i )  )
              ; isNTrans = record { commute = comm1 }
       } where
-    iid :  {i : Obj C } → Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
-    iid {i} = FMap Γ ( small-iso s ) 
+    iso1 :   {a b : Obj C} {f : Hom C a b} →  C [ f o small-iso s ] ≡ C [ small-iso s o shom← s (shom→ s f) ]
+    iso1 = {!!}
     comm1 :  {a b : Obj C} {f : Hom C a b} →
-        Sets [ Sets [ FMap Γ f o (λ sn → iid (snmap sn (small→ s a))) ] ≈
-        Sets [ (λ sn → iid (snmap sn (small→ s b))) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+        Sets [ Sets [ FMap Γ f o (λ sn → iid s Γ (snmap sn (small→ s a))) ] ≈
+        Sets [ (λ sn → iid s Γ (snmap sn (small→ s b))) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
     comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
-                 FMap Γ f ( iid (snmap sn (small→ s a)) )
-             ≡⟨ {!!} ⟩
-                iid ( (ΓMap s Γ (shom→ s  f))  ( snmap sn ( small→ s a )) )
-             ≡⟨ ≡cong ( λ y → iid y ) ( sncommute sn (shom→ s  f) )  ⟩
-                 iid (snmap sn (small→ s b))
+                 FMap Γ f ( ( FMap Γ ( small-iso s ) ) (snmap sn (small→ s a)) )
+             ≡⟨⟩
+                 ( Sets [ FMap Γ f o  FMap Γ ( small-iso s ) ] ) (snmap sn (small→ s a)) 
+             ≡⟨ ≡cong (λ z → z (snmap sn (small→ s a))  ) (sym ( IsFunctor.distr (isFunctor Γ ) ))  ⟩
+                 FMap Γ ( C [ f o  (small-iso s) ] ) (snmap sn (small→ s a) )
+             ≡⟨  ≡cong (λ z → ( FMap Γ z ) (snmap sn (small→ s a))) iso1 ⟩
+                 FMap  Γ ( C [ (small-iso s) o   shom← s (shom→ s f)  ]  )  ( snmap sn ( small→ s a )) 
+             ≡⟨  ≡cong (λ z → z (snmap sn (small→ s a))  ) ( IsFunctor.distr (isFunctor Γ ) )  ⟩
+                 ( Sets [  FMap  Γ (small-iso s) o  FMap Γ  (shom← s (shom→ s f)) ]  )  ( snmap sn ( small→ s a )) 
+             ≡⟨⟩
+                 ( Sets [  FMap  Γ (small-iso s) o  (ΓMap s Γ (shom→ s  f)) ]  )  ( snmap sn ( small→ s a )) 
+             ≡⟨⟩
+                 FMap  Γ (small-iso s)  ((ΓMap s Γ (shom→ s  f))  ( snmap sn ( small→ s a )) )
+             ≡⟨ ≡cong ( λ y → iid s Γ y ) ( sncommute sn (shom→ s  f) )  ⟩
+                 FMap  Γ (small-iso s) (snmap sn (small→ s b))
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -204,7 +232,7 @@
     → Limit Sets C Γ
 SetsLimit { c₂} C I s Γ = record { 
            a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
-         ; t0 = SetsNat C I s Γ
+         ; t0 = Cone C I s Γ
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = {!!}