Mercurial > hg > Members > kono > Proof > category

changeset 583:cd65d5c9a54d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
anothter approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 May 2017 18:14:49 +0900
parents c9361d23aa3a
children f0f516817762
files SetsCompleteness.agda
diffstat 1 files changed, 19 insertions(+), 101 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Apr 29 22:22:20 2017 +0900
+++ b/SetsCompleteness.agda	Wed May 03 18:14:49 2017 +0900
@@ -176,123 +176,41 @@
 slid :   {  c₁  : Level}  { I :  Set  c₁ }  →   I → I
 slid x = x
 
-record slim  { 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 ) 
+                (lim :   Set  c₂ ) ( e : lim → sproduct OC sobj  ) 
       :  Set   c₂  where
    field 
-       slequ : { i j : OC } → ( f :  I → I ) →  sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
-   ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj
-   ipp {i} {j} f = equ ( slequ {i} {j} f )
-   slobj : OC →  Set  c₂ 
-   slobj i = sobj i
-   llr :  {i j : OC } → ( f : I → I ) →  proj ( equ ( slequ {i} {i} slid )) i ≡ proj ( equ ( slequ {i} {j} f )) i 
-   llr {i} {j} f = ?
-   lll :  {i j  : OC } → ( f : I → I ) →  proj ( equ ( slequ {i} {j} f )) j ≡ proj ( equ ( slequ {j} {j} slid )) j 
-   lll  {i} {j} f  = {!!}
-   ll :  {x i j i' j' : OC } → ( f f' : I → I ) →  proj ( equ ( slequ {i} {j} f )) x ≡ proj ( equ ( slequ {i'} {j'} f' )) x 
-   ll {x} {i} {j} {i'} {j'} f f' = begin
-           proj ( equ {_} {sproduct OC sobj } {sobj j} ( slequ {i} {j} f )) x 
-        ≡⟨ {!!} ⟩
-           proj ( equ {_} {sproduct OC sobj } {sobj j'} ( slequ {i'} {j'} f' )) x 
-        ∎   where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-
-   -- slmap : {i j : OC } →  (f : I → I ) → sobj i → sobj j
-   -- slmap f = smap f 
+       slequ :  (i j : OC) (f :  I → I  ) → sequ lim (sobj j) (λ x →  smap f (proj (e x) i) ) (λ x → proj (e x) j )
 
 open slim
 
-lemma-equ :   {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
-    {x i j i' j' : Obj C } →　 { f f' : I → I } 
-    →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
-    →  proj (ipp se {i} {j} f) x ≡ proj (ipp se {i'} {j'} f' ) x
-lemma-equ C I s Γ {x} {i} {j} {i'} {j'} {f} {f'} se =   ll se f f'
-
-
 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 (slim (ΓObj s Γ) (ΓMap s Γ)  )) Γ
-Cone C I s  Γ =  record {
-               TMap = λ i →  λ se → proj ( ipp se {i} {i} slid ) i
+    → ( lim :  Set  c₁ )
+    → ( e : Hom Sets lim (sproduct (Obj C) (ΓObj s  Γ)) )
+    → NTrans C Sets (K Sets C lim) Γ
+Cone C I s  Γ lim e  =  record {
+               TMap = λ i →  λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s  Γ)}  {FObj Γ i}
+                     {λ x → proj x i} {λ x → proj x i} (elem (e se ) refl )) i
              ; isNTrans = record { commute = commute1 }
       } where
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se  slid ) a) ] ≈
-                Sets [ (λ se → proj ( ipp se  slid ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
+         cone-equ : (a b : Obj C) (f : Hom C a b) → (se : lim ) → sequ lim (FObj Γ b) (λ x →  FMap Γ f (proj (e x) a) ) (λ x → proj (e x) b )
+         cone-equ a b f se = slequ ? ? ? ?
+         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (equ (elem (e se) refl)) a) ]
+              ≈ Sets [ (λ se → proj (equ (elem (e se) refl)) b) o FMap (K Sets C lim) f ] ]
          commute1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
-                   (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se  slid ) a) ]) se
+                 (Sets [ FMap Γ f o (λ se → proj (equ (elem (e se) refl)) a) ]) se
              ≡⟨⟩
-                   FMap Γ f (proj ( ipp se {a} {a} slid ) a)
-             ≡⟨  ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} slid ) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {a} slid ) a)
-             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ {a} se ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {b} (hom→ s f) ) a)
-             ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
-                   proj (ipp se {a} {b} ( hom→ s f  )) b
-             ≡⟨ sym ( lemma-equ C I s Γ {b} se ) ⟩
-                   proj (ipp se {b} {b} (λ x → x)) b
+                  FMap Γ f (proj (e se) a )
+             ≡⟨  fe=ge0 (cone-equ a b f se ) ⟩
+                  proj (e se) b 
              ≡⟨⟩
-                  (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
+                  (Sets [ (λ se → proj (equ (elem (e se) refl)) b) o FMap (K Sets C lim) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
 
-
-
-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 =  slim  (ΓObj s Γ) (ΓMap s Γ)  
-         ; t0 = Cone C I s Γ 
-         ; isLimit = record {
-               limit  =  limit1 
-             ; t0f=t = λ {a t i } → refl
-             ; limit-uniqueness  =  λ {a} {t} {f} → uniquness1 {a} {t} {f}
-          }
-       }  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 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 {
-                   slequ = λ {i} {j} f → elem ( record { proj = λ 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 (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 ) 
-                     →  record { proj = λ i₁ → TMap t i₁ x }  ≡ equ (slequ (f x) f')
-              uniquness2 {a} {t} {f} i j cif=t f' x = begin
-                  record { proj = λ i → TMap t i x }
-                ≡⟨   ≡cong ( λ g → record { proj = λ i → g i  } ) (  extensionality Sets  ( λ i →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
-                  record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
-                ≡⟨⟩
-                  record { proj = λ i →   proj (ipp (f x) {i} {i} slid ) i }
-                ≡⟨ ≡cong ( λ g →   record { proj = λ i' →  g i' } ) ( extensionality Sets  ( λ  i''  → lemma-equ C I s Γ {i''} (f x)))  ⟩
-                  record { proj = λ i →  proj (ipp (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 (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 { slequ = λ {i} {j} f' → elem ( record { proj = λ 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 { proj = λ i → TMap t i x }  ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' x ) )
-                           )))
-                     ) ⟩
-                   record { slequ = λ {i} {j} f' → slequ (f x ) f'  }
-                ≡⟨⟩
-                  f x
-                ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-