Mercurial > hg > Members > kono > Proof > category

changeset 552:09b1f66f7d7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 08 Apr 2017 11:35:51 +0900
parents 97b98b81e990
children e33282817cb7
files SetsCompleteness.agda
diffstat 1 files changed, 14 insertions(+), 75 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu Apr 06 04:15:57 2017 +0900
+++ b/SetsCompleteness.agda	Sat Apr 08 11:35:51 2017 +0900
@@ -153,8 +153,8 @@
 record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-     hom→ : {i j : Obj C } →    Hom C i j →  I  
-     hom← : {i j : Obj C } →  ( f : I ) →  Hom C i j 
+     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 
      -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
 
@@ -165,83 +165,29 @@
 Γ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 : Obj C } →　 ( f : 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 Γ ( 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
+record snat  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j )
+     ( Equ : { i j :  OC  }  →  { f : I → I } →   sequ (sobj i) (sobj j) ( smap f ) ( smap (λ x → x ) )) :  Set   c₂  where
    field 
        snmap : ( i : OC ) → sobj i 
-       sncommute : { i j : OC } → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
+       sncommute : { i j : OC } → ( f :  I → I ) →  smap f ( snmap i )  ≡ snmap j
 
 open snat
 
-snmeq :  { c₂ : Level } { I OC :  Set  c₂ } { SO :  OC →  Set   c₂  } { SM : { i j :  OC  }  → (f : I )→  SO i → SO j }
-          ( s t :  snat SO SM  ) → ( i : OC ) → 
-         { snmapsi   snmapti : SO i } →  snmapsi ≡  snmapti → SO i
-snmeq s t i {pi} {.pi} refl   = pi
-
-snat1 :   { c₂ : Level }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j )
-    ( s t :  snat sobj smap )
-    ( eq1 : ( i : OC ) →  snmap s i ≡  snmap t i ) →  
-     (( i j :  OC  )  → (f : I ) → smap f (snmeq s t i (eq1 i) ) ≡ (snmeq s t j (eq1 j)  )) → snat sobj smap
-snat1 SO SM s t eq1 eqcomm = record { snmap = λ i → snmeq s t i (eq1 i);   sncommute = λ {i} {j} f → eqcomm i j f   }
-
-≡cong2 : { c : Level } { A B C : Set  c } { a a' : A } { b b' : B } ( f : A → B → C ) 
-    →  a  ≡  a'
-    →  b  ≡  b'
-    →  f a b  ≡  f a' b'
-≡cong2 _ refl refl = refl
-
-snat-cong :  { c : Level }  { I OC :  Set  c }  ( SObj :  OC →  Set  c  ) ( SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j)  
-         { s t :  snat SObj SMap   }
-     → (( i : OC ) → snmap s i ≡  snmap t i )
-     → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap s i )   ≡ snmap s j )
-     → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap t i )   ≡ snmap t j )
-     → s ≡ t
-snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 =  ≡cong ( λ x  → snat1 SO SM s t eq1 x  ) 
-                 ( extensionality Sets  ( λ  i  →  
-                 ( extensionality Sets  ( λ  j  →  
-                 ( extensionality Sets  ( λ  f  →   irr2 (λ i →  snmeq s t i (eq1 i) )i j f ( eq2s i j f (eq1 i)  (λ i →  snmeq s t i (eq1 i) ){!!} {!!} (eq2 i j f ) ) {!!} ))))))
-   where
-      eq2s1 : { i j : OC } { f : I }  →  {si : SO i} { sj : SO j } 
-           ( snm : ( i : OC ) → SO i ) → ( si ≡  snm i ) → ( sj ≡  snm j ) → SM {i} {j} f  si ≡ sj →  SM f ( snm i) ≡ snm j
-      eq2s1 {i} {j} {f} {si} {sj}  snm eq1 eq2 eq3 =  begin
-                 SM f ( snm i)  
-             ≡⟨ ≡cong (λ x → SM f x ) (sym eq1)  ⟩
-                 SM f si  
-             ≡⟨ eq3 ⟩
-                 sj  
-             ≡⟨ eq2 ⟩
-                snm j
-             ∎   where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-      eq2s : ( i j : OC ) ( f : I )  →   ( snmap s i ≡  snmap t i ) → 
-           ( snm : ( i : OC ) → SO i ) 
-            → snmap s i  ≡ snm i → snmap s j  ≡ snm j 
-            → SM {i} {j} f ( snmap s i )   ≡ snmap s j →  SM f ( snm i) ≡ snm j
-      eq2s i j f eq1 snm eq2 eq3 eq4   =  eq2s1 snm eq2 eq3 eq4
-      irr3 : { i j : OC } { f : I }  →  {snmapsi :  SO i  }  → {snmapsj :  SO j  } →
-           ( es et : SM f ( snmapsi )  ≡ snmapsj  )  → es  ≡ et
-      irr3 refl refl = refl
-      irr2 :  ( snm : ( i : OC ) → SO i ) ( i j : OC ) (f : I )  →  
-              ( es et : SM f (snm i )  ≡ snm j ) →  es  ≡ et 
-      irr2 snm i j f  es et = irr3 es et 
-
-
 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 (snat  (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
+    → NTrans C Sets (K Sets C (snat  (ΓObj s Γ) (ΓMap s Γ) {!!} ) ) Γ
 Cone C I s  Γ  =  record {
                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 → snmap sn a) ] ≈
-        Sets [ (λ sn →  (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+        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 ( hom-iso s  )) ⟩
@@ -258,7 +204,7 @@
 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 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
+           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ)  {!!}
          ; t0 = Cone C I s Γ
          ; isLimit = record {
                limit  = limit1
@@ -267,11 +213,11 @@
           }
        }  where
           a0 : Obj Sets
-          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
-          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) 
+          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) {!!} 
+          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 : 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 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 ]
@@ -284,13 +230,13 @@
              ∎  ) 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 Γ))} →
+          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 {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 }
-             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) {!!}  {!!} {!!} ⟩
+             ≡⟨ {!!} (ΓObj s Γ) (ΓMap s Γ) {!!}  {!!} {!!} ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
              ≡⟨⟩
                   f x
@@ -299,10 +245,3 @@
                   open ≡-Reasoning
 
 
-
-
-
-
-
-
-