Mercurial > hg > Members > kono > Proof > category

changeset 538:d22c93dca806

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
locally small
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Mar 2017 08:01:13 +0900
parents 2f261a3836bc
children 9a657775d81e
files SetsCompleteness.agda
diffstat 1 files changed, 26 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu Mar 30 18:11:11 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 31 08:01:13 2017 +0900
@@ -146,44 +146,32 @@
 
 open Functor
 
+----
+-- C is locally small i.e. Hom C i j is a set c₁
+--
 record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-     small→ : Obj C → I
-     small← : I → Obj C
-     small-iso : { x : Obj C  } → Hom 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 )
-     iso1 :   {a b : Obj C} {f : Hom C a b} →  C [ f o small-iso  ] ≡ C [ small-iso  o shom←  (shom→  f) ]
-
-     -- iso1 should be proved by these ...
-     -- small-≡   : { x : Obj C  } →  (small← ( small→ x )) ≡ x
-     -- shom-iso : {i j : I } →  ( f : Hom C ( small←  i  ) (  small←  j ) ) →  C [ shom← ( shom→ f )  ≈ f ]
+     shom→ : {i j : Obj C } →    Hom C i j →  I → I 
+     shom← : {i j : Obj C } →  ( f : I → I ) →  Hom C i j 
+     shom-iso : {i j : Obj C } →  { f : Hom C i j } →   shom← ( shom→ f )  ≡ f 
      -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
 
 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
-
-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 )
+   (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 : I } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
+    {i j : Obj C } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
 ΓMap  s Γ {i} {j} f = FMap Γ ( shom← s f ) 
 
-record snat   { c₂ }  { I :  Set  c₂ } ( sobj :  I →  Set  c₂ ) 
-     ( smap : { i j :  I  }  → (f : I → I )→  sobj i → sobj j ) : Set  c₂ where
+record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) 
+     ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) : Set  c₂ where
    field 
-       snmap : ( i : I ) → sobj i 
-       sncommute : { i j : I } → ( f : I → I ) →  smap f ( snmap i )  ≡ snmap j
+       snmap : ( i : OC ) → sobj i 
+       sncommute : { i j : OC } → ( f : I → I ) →  smap f ( snmap i )  ≡ snmap j
 
 open snat
 
@@ -194,28 +182,20 @@
 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 →  iid s Γ ( snmap sn (small→ s i )  )
+               TMap = λ i →  λ sn →  snmap sn i 
              ; isNTrans = record { commute = comm1 }
       } where
     comm1 :  {a b : Obj C} {f : Hom C a b} →
-        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 ] ]
+        Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
+        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 ( ( FMap Γ ( small-iso s ) ) (snmap sn (small→ s a)) )
+                 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 )
              ≡⟨⟩
-                 ( 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 s) ⟩
-                 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))
+                 ΓMap s Γ (shom→ s f) (snmap sn a ) 
+             ≡⟨ sncommute sn (shom→ s  f) ⟩
+                 snmap sn b
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -235,11 +215,11 @@
        }  where
           a0 : Obj Sets
           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
-          comm2 : { a : Obj Sets } {x : a } {i j : I} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I) 
-             → ΓMap s Γ f (TMap t (small← s i) x) ≡ TMap t (small← s j) x
-          comm2 = {!!}
+          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → 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 t = λ x →  record { snmap = λ i →  ( TMap t ( small← s i ) ) x ;
+          limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
               sncommute = λ f → comm2 t f }