Mercurial > hg > Members > kono > Proof > category

changeset 673:0007f9a25e9c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix limit from product and equalizer (not yet finished )
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Nov 2017 13:31:08 +0900
parents 749df4959d19
children 77690b17c5d9
files SetsCompleteness.agda cat-utility.agda pullback.agda
diffstat 3 files changed, 79 insertions(+), 61 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu Nov 02 09:00:01 2017 +0900
+++ b/SetsCompleteness.agda	Fri Nov 03 13:31:08 2017 +0900
@@ -52,10 +52,9 @@
 open iproduct
 
 SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
-     → IProduct ( Sets  {  c₂} ) I
+     → IProduct ( Sets  {  c₂} ) I ai
 SetsIProduct I fi = record {
-       ai =  fi
-       ; iprod = iproduct I fi
+       iprod = iproduct I fi
        ; pi  = λ i prod  → pi1 prod i
        ; isIProduct = record {
               iproduct = iproduct1
--- a/cat-utility.agda	Thu Nov 02 09:00:01 2017 +0900
+++ b/cat-utility.agda	Fri Nov 03 13:31:08 2017 +0900
@@ -248,9 +248,8 @@
                    iproduct qi
                  ∎
 
-        record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  ( I : Set c) : Set  (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
+        record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  ( I : Set c) (ai : I → Obj A) : Set  (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
             field
-              ai : I → Obj A 
               iprod :  Obj A
               pi : (i : I ) → Hom A iprod  ( ai i )  
               isIProduct :  IsIProduct A I iprod  ai  pi  
@@ -362,7 +361,7 @@
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
              climit :  ( Γ : Functor I A ) → Limit A I Γ 
-             cproduct : ( I : Set c₁' ) (fi : I → Obj A )  → IProduct A I -- c₁ should be a free level
+             cproduct : ( I : Set c₁' ) (fi : I → Obj A )  → IProduct A I fi -- c₁ should be a free level
              cequalizer : {a b : Obj A} (f g : Hom A a b)  → Equalizer A  f g
           open Limit
           limit-c :  ( Γ : Functor I A ) → Obj A
--- a/pullback.agda	Thu Nov 02 09:00:01 2017 +0900
+++ b/pullback.agda	Fri Nov 03 13:31:08 2017 +0900
@@ -29,7 +29,6 @@
 open Equalizer
 open IsEqualizer
 open IsProduct
-open Pullback
 
 pullback-from :  (a b c ab d : Obj A)
       ( f : Hom A a c )    ( g : Hom A b c )
@@ -223,9 +222,8 @@
 
 limit2couniv :
      ( lim : ( Γ : Functor I A ) → Limit A I Γ )
-     → ( aΓ : ( Γ : Functor I A ) → Obj A ) ( tΓ :  ( Γ : Functor I A ) → NTrans I A ( K A I (aΓ Γ) ) Γ )
      →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → a0 ( lim b) )  ( λ b → t0 (lim b)  )
-limit2couniv lim aΓ tΓ = record {  -- F             U                            ε
+limit2couniv lim  = record {  -- F             U                            ε
        _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; -- η
        iscoUniversalMapping = record {
            couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
@@ -258,7 +256,7 @@
 univ2limit :
      ( U : Obj (A ^ I ) → Obj A )
      ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b )
-     ( univ :  coUniversalMapping A (A ^ I) (KI I) U (ε) ) →
+     ( univ :  coUniversalMapping A (A ^ I) (KI I) U ε ) →
      ( Γ : Functor I A ) →   Limit A I Γ 
 univ2limit U ε univ Γ = record {
      a0 = U Γ ;
@@ -322,89 +320,111 @@
 --                                              Γ f o ε i = ε j 
 --
 
+equc : ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
+        ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
+            → Obj A
+equc prod eqa = equalizer-c (eqa p0id p0id)
+   where
+         p0 = iprod (prod (FObj Γ))
+         p0id = let  open ≈-Reasoning (A) in id1 A p0 
+
+equproj : ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
+   (i : Obj I ) → Hom A (iprod (prod (FObj Γ))) (FObj Γ i)  
+equproj prod i = pi (prod (FObj Γ)) i 
+
 limit-ε :
-     ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → IsEqualizer A e f g )
-     ( lim p : Obj A ) ( e : Hom  A lim p )
-     ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
-         NTrans I A (K A I lim) Γ
-limit-ε eqa lim p e proj = record {
-      TMap = tmap ;
-      isNTrans = record { commute = commute1 }
-  } where
-      tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
-      tmap i = A [ proj i o e ]
-      commute1 :  {i j : Obj I} {f : Hom I i j} →
-        A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ]
-      commute1 {i} {j} {f} =  let  open ≈-Reasoning (A) in begin
-             FMap Γ f o tmap i 
-        ≈⟨⟩
-             FMap Γ f o ( proj i o e )
-        ≈⟨ assoc ⟩
-             ( FMap Γ f o  proj i ) o e 
-        ≈⟨ fe=ge ( eqa e (FMap Γ f o  proj i) ( proj j ))  ⟩
-             proj j o e 
-        ≈↑⟨ idR ⟩
-             (proj j o e ) o id1 A lim
-        ≈⟨⟩
-             tmap j o FMap (K A I lim) f
-        ∎  
+     ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
+     ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
+          → NTrans I A (K A I (equc prod eqa )) Γ
+limit-ε prod eqa = record {
+       TMap = λ i → tmap i ; 
+       isNTrans = record { commute = commute1 }
+   } where
+       lim = equc prod eqa
+       p0 = iprod (prod (FObj Γ))
+       e = let  open ≈-Reasoning (A) in equalizer ( eqa (id1 A p0 ) ( id1 A p0 ) )
+       proj = pi ( prod  (FObj Γ) )
+       tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
+       tmap i = A [ equproj prod i o e ] 
+       commute1 :  {i j : Obj I} {f : Hom I i j} →
+         A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ]
+       commute1 {i} {j} {f} =  let  open ≈-Reasoning (A) in begin
+              FMap Γ f o tmap i 
+         ≈⟨⟩
+              FMap Γ f o ( proj i o e )
+         ≈⟨ assoc ⟩
+              ( FMap Γ f o  proj i ) o e 
+         -- ≈⟨ fe=ge (isEqualizer (eqa (FMap Γ f o  proj i) ( proj j ))) ⟩
+         ≈⟨ {!!} ⟩
+              proj j o e 
+         ≈↑⟨ idR ⟩
+              (proj j o e ) o id1 A lim
+         ≈⟨⟩
+              tmap j o FMap (K A I lim) f
+         ∎
 
 limit-from :
-     ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
-                  →  IsIProduct {c₁'} A (Obj I) p ai pi )
-     ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → IsEqualizer A e f g )
-     ( lim p : Obj A )       -- limit to be made
-     ( e : Hom  A lim p )                          -- existing of equalizer
-     ( proj : (i : Obj I ) → Hom A p (FObj Γ i) )  -- existing of product ( projection actually )
+     ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
+     ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
       → Limit A I Γ 
-limit-from prod eqa lim p e proj = record {
-     a0 = lim ;
-     t0 = limit-ε eqa lim p e proj ;
+limit-from prod eqa = record {
+     a0 = equalizer-c p0equ ;
+     t0 = limit-ε prod eqa ; 
      isLimit = record {
              limit = λ a t → limit1 a t ;
-             t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
+             t0f=t = λ {a t i } → t0f=t1  {a} {t} {i} ;
              limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
     }  where
+         lim : Obj A 
+         lim = equc prod eqa 
+         p0 = iprod (prod (FObj Γ))
+         p0id = let  open ≈-Reasoning (A) in id1 A p0 
+         p0equ = eqa p0id p0id
+         e = let  open ≈-Reasoning (A) in equalizer ( eqa (id1 A p0 ) ( id1 A p0 ) )
+         equ = isEqualizer (eqa (id1 A p0) (id1 A p0 ))
+         proj = pi ( prod  (FObj Γ) )
+         prodΓ = isIProduct ( prod (FObj Γ) ) 
          limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
-         limit1 a t = let  open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (iproduct ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
+         limit1 a t = let  open ≈-Reasoning (A) in k equ (iproduct prodΓ (TMap t) ) refl-hom
          t0f=t1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
-                A [ A [ TMap (limit-ε eqa lim p e proj ) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap (limit-ε prod eqa ) i o limit1 a t ] ≈ TMap t i ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in begin
-                   TMap (limit-ε eqa lim p e proj ) i o limit1 a t 
+                   TMap (limit-ε prod eqa ) i o limit1 a t 
                 ≈⟨⟩
-                   ( ( proj i )  o e ) o  k (eqa e (id1 A p) (id1 A p )) (iproduct ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
+                   ( ( proj i )  o e ) o  k equ (iproduct prodΓ (TMap t) ) refl-hom
                 ≈↑⟨ assoc  ⟩
-                    proj i  o ( e  o  k (eqa e (id1 A p) (id1 A p )) (iproduct ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom )
-                ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩
-                    proj i  o iproduct (prod p (FObj Γ) proj) (TMap t)
-                ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩
+                    proj i  o ( e  o  k equ (iproduct prodΓ (TMap t) ) refl-hom )
+                ≈⟨ cdr ( ek=h equ) ⟩
+                    proj i  o iproduct prodΓ (TMap t)
+                ≈⟨ pif=q prodΓ (TMap t) ⟩
                    TMap t i 
                 ∎
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} 
-                → ({i : Obj I} → A [ A [ TMap (limit-ε eqa lim p e proj ) i o f ] ≈ TMap t i ]) →
+                → ({i : Obj I} → A [ A [ TMap (limit-ε prod eqa ) i o f ] ≈ TMap t i ]) →
                 A [ limit1 a t ≈ f ]
          limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in begin
                     limit1 a t
                 ≈⟨⟩
-                    k (eqa e (id1 A p) (id1 A p )) (iproduct ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
-                ≈⟨ IsEqualizer.uniqueness  (eqa e (id1 A p) (id1 A p )) ( begin
+                    k equ (iproduct prodΓ (TMap t) ) refl-hom
+                ≈⟨ IsEqualizer.uniqueness  equ ( begin
                       e o f 
-                ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩
-                      iproduct (prod p (FObj Γ) proj) (λ i → ( proj i o ( e  o f ) ) )
-                ≈⟨ ip-cong  (prod p (FObj Γ) proj) ( λ i → begin
+                ≈↑⟨ ip-uniqueness prodΓ ⟩
+                      iproduct prodΓ (λ i → ( proj i o ( e  o f ) ) )
+                ≈⟨ ip-cong  prodΓ ( λ i → begin
                         proj i o ( e o f )
                 ≈⟨ assoc  ⟩
                         ( proj i o  e ) o f 
                 ≈⟨ lim=t {i} ⟩
                         TMap t i
                 ∎ ) ⟩
-                      iproduct (prod p (FObj Γ) proj) (TMap t)
+                      iproduct prodΓ (TMap t)
                 ∎ ) ⟩
                     f
                 ∎
 
-----
+
+--
 --
 -- Adjoint functor preserves limits
 --