Mercurial > hg > Members > kono > Proof > category

changeset 570:3d6d8fea3e09

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
yelloow remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Apr 2017 20:44:21 +0900
parents 25c18786fbdc
children 143de0e3eb60
files SetsCompleteness.agda
diffstat 1 files changed, 46 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 24 12:17:41 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 24 20:44:21 2017 +0900
@@ -53,7 +53,7 @@
 
 open iproduct
 
-SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) 
+SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (fi : I → Obj Sets ) 
      → IProduct ( Sets  {  c₂} ) I
 SetsIProduct I fi = record {
        ai =  fi
@@ -185,43 +185,54 @@
 
 open snproj
 
-record snequ  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) 
+record slim  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) 
       :  Set   c₂  where
    field 
-       snequ1 : { i j : OC } → ( f :  I → I ) →  sequ (snproj sobj smap ) (sobj j) ( λ x → smap f ( snmap x i ) ) (  λ x → snmap x j )
+       slequ : { i j : OC } → ( f :  I → I ) →  sequ (snproj sobj smap ) (sobj j) ( λ x → smap f ( snmap x i ) ) (  λ x → snmap x j )
+   slobj : OC →  Set  c₂ 
+   slobj i = sobj i
 
-open snequ
+open slim
 
 open import HomReasoning
 open NTrans
 
 lemma-equ : {  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 : snequ (ΓObj s Γ) (ΓMap s Γ)  }
-          → snmap (equ (snequ1 se {a} {a} (λ x → x))) a ≡ snmap (equ (snequ1 se {a} {b} f )) a 
-lemma-equ = {!!}
+      {a b : Obj C  } { f : I → I }  { se : slim (ΓObj s Γ) (ΓMap s Γ)  }
+          → snmap (equ (slequ se {a} {a} (λ x → x))) a ≡ snmap (equ (slequ se {a} {b} f )) a 
+lemma-equ C I s Γ {a} {b} {f} {se} = begin
+                  snmap (equ (slequ se {a} {a} (λ x → x))) a
+             ≡⟨ ≡cong ( λ p → snmap p a )  (  ≡cong ( λ QIX → record { snmap = QIX } ) (  
+                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  )  refl
+              ) )) ⟩
+                  snmap (equ (slequ se {a} {b} f )) a
+             ∎   where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
 
 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 (snequ (ΓObj s Γ) (ΓMap s Γ) )) Γ
+    → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) Γ
 Cone C I s  Γ =  record {
-               TMap = λ i →  λ se → snmap (equ (snequ1 se {i} {i} (λ x → x )) ) i
+               TMap = λ i →  λ se → snmap (equ (slequ se {i} {i} (λ x → x )) ) i
              ; isNTrans = record { commute = commute1 }
       } where
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → snmap (equ (snequ1 se {a} {a} (λ x → x))) a) ] ≈
-                Sets [ (λ se → snmap (equ (snequ1 se {b} {b} (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → snmap (equ (slequ se {a} {a} (λ x → x))) a) ] ≈
+                Sets [ (λ se → snmap (equ (slequ se {b} {b} (λ x → x))) 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₁ → snmap (equ (snequ1 se₁ (λ x → x))) a) ]) se
+                   (Sets [ FMap Γ f o (λ se₁ → snmap (equ (slequ se₁ (λ x → x))) a) ]) se
              ≡⟨⟩
-                   FMap Γ f (snmap (equ (snequ1 se (λ x → x))) a)
-             ≡⟨  ≡cong ( λ g → FMap Γ g (snmap (equ (snequ1 se (λ x → x))) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (snequ1 se {a} {a} (λ x → x))) a)
+                   FMap Γ f (snmap (equ (slequ se (λ x → x))) a)
+             ≡⟨  ≡cong ( λ g → FMap Γ g (snmap (equ (slequ se (λ x → x))) a))  (sym ( hom-iso s  ) ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (slequ se {a} {a} (λ x → x))) a)
              ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ C I s Γ  )   ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (snequ1 se (hom→ s f ))) a)
-             ≡⟨  fe=ge0 ( snequ1 se (hom→ s f ) ) ⟩
-                   snmap (equ (snequ1 se ( hom→ s f ) )) b
+                   FMap Γ  (hom← s ( hom→ s f))  (snmap (equ (slequ se (hom→ s f ))) a)
+             ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
+                   snmap (equ (slequ se ( hom→ s f ) )) b
              ≡⟨ sym ( lemma-equ C I s Γ )  ⟩
-                   snmap (equ (snequ1 se (λ x → x))) b
+                   snmap (equ (slequ se (λ x → x))) b
              ≡⟨⟩
-                  (Sets [ (λ se₁ → snmap (equ (snequ1 se₁ (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ]) se
+                  (Sets [ (λ se₁ → snmap (equ (slequ se₁ (λ x → x))) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -231,7 +242,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 =  snequ  (ΓObj s Γ) (ΓMap s Γ)  
+           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ)  
          ; t0 = Cone C I s Γ 
          ; isLimit = record {
                limit  =  limit1 
@@ -241,40 +252,41 @@
        }  where
               limit2 :  (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → {i j : Obj C } →　 ( f : I → I ) 
                     → ( x : a )  → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
-              limit2 a t {i} {j} f x =   ≡cong ( λ g → g x )   ( IsNTrans.commute ( isNTrans t  ) )
-              limit1 :  (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ))
+              limit2 a t f x =   ≡cong ( λ g → g x )   ( IsNTrans.commute ( isNTrans t  ) )
+              limit1 :  (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ))
               limit1 a t x = record {
-                   snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x  )
+                   slequ = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x  )
                 } 
-              uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ) )} →
+              uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )} 
+                     →  ( i j : Obj C  ) →
                     ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) →  (f' : I → I ) →  (x : a ) 
-                     →  equ (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t f' x)) ≡ equ (snequ1 (f x) f')
-              uniquness2 {a} {t} {f} cif=t f' x = begin
+                     →  equ (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t {i} {j} f' x)) ≡ equ (slequ (f x) f')
+              uniquness2 {a} {t} {f} i j cif=t f' x = begin
                   record { snmap = λ i₁ → TMap t i₁ x }
                 ≡⟨   ≡cong ( λ g → record { snmap = λ i → g i  } ) (  extensionality Sets  ( λ  i  →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
                   record { snmap = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
                 ≡⟨⟩
-                  record { snmap = λ i →   snmap (equ (snequ1 (f x) {i} {i} (λ x → x )) ) i }
+                  record { snmap = λ i →   snmap (equ (slequ (f x) {i} {i} (λ x → x )) ) i }
                 ≡⟨ ≡cong ( λ g →   record { snmap = λ i →  g i  } ) (  extensionality Sets  ( λ  i  → lemma-equ C I s Γ ))  ⟩
-                  record { snmap = λ i₁ →  snmap (equ (snequ1 (f x) f')) i₁  }
+                  record { snmap = λ i₁ →  snmap (equ (slequ (f x) f')) i₁  }
                 ∎   where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
-              uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ) )} →
+              uniquness1 : {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 ]
               uniquness1 {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
                   limit1 a t x
                 ≡⟨⟩
-                   record { snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x ) }
-                ≡⟨ ≡cong ( λ e → record { snequ1 =  λ {i} {j} f' → e i j f' x } ) (
+                   record { slequ = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x ) }
+                ≡⟨ ≡cong ( λ e → record { slequ =  λ {i} {j} f' → e i j f' x } ) (
                         extensionality Sets  ( λ  i  →
                            extensionality Sets  ( λ  j  →
                                extensionality Sets  ( λ  f'  →
                                    extensionality Sets  ( λ  x  → 
-                  elm-cong (  elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f' x )) (snequ1 (f x) f' ) (uniquness2 cif=t f' x ) )
+                  elm-cong (  elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 i j cif=t f' x ) )
                            )))
                      ) ⟩
-                   record { snequ1 = λ {i} {j} f' → snequ1 (f x ) f' }
+                   record { slequ = λ {i} {j} f' → slequ (f x ) f' }
                 ≡⟨⟩
                   f x
                 ∎  ) where