Mercurial > hg > Members > kono > Proof > category

changeset 281:dbd2044add2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit from product and equalizer continue...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 13:21:59 +0900
parents 7ae58263d45b
children c831abfa9bf4
files pullback.agda
diffstat 1 files changed, 44 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 10:57:39 2013 +0900
+++ b/pullback.agda	Mon Sep 23 13:21:59 2013 +0900
@@ -305,13 +305,48 @@
             f
         ∎
 
+-----
+--
+-- product on arbitrary index
+--
+
+record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  ( I : Set c)
+      ( p  : Obj A )                       -- product
+      ( ai : I → Obj A )                   -- families
+      ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections
+            : Set  (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
+   field
+      product : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
+      pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( product qi ) ] ≈  (qi i) ]
+      ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
+      ip-cong : {q : Obj A}   → ( qi : (i : I) → Hom A q (ai i) ) → ( qi' : (i : I) → Hom A q (ai i) )
+                → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ] 
+
+open IProduct 
+
+limit-equalizer :  
+      ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
+                  →  IProduct {c₁'} A (Obj I) p ai pi )
+      ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g ) 
+     ( Γ : Functor I A ) →   
+     ( lim : Obj A ) 
+     ( proj : (i : Obj I ) → Hom A lim (FObj Γ i) ) → 
+         NTrans I A (K I lim) Γ
+limit-equalizer prod eqa Γ lim proj = record {
+      TMap = tmap ; 
+      isNTrans = record {
+          commute = {!!}
+      }
+  } where
+      tmap : (i : Obj I) → Hom A (FObj (K I lim) i) (FObj Γ i)
+      tmap i = A [ ( proj i )  o equalizer ( eqa (id1 A lim) (A [ FMap Γ (id1 I i) o proj i ] ) (A [ {!!} o {!!} ] )) ]
+
 limit-from :  
-      ( prod : (a b ab  : Obj A) ( π1 : Hom A ab a )  ( π2 : Hom A ab b ) 
-                  →  Product A a b ab π1 π2 ) 
-      ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g ) 
-          -- ( A [  π1 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] )
-          -- ( A [  π2 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] ) 
-     ( U : Obj (A ^ I ) → Obj A ) 
-     ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K I (U b)) b ) →
-     ( Γ : Functor I A ) →   Limit I Γ (U Γ) (ε Γ)
-limit-from proc eqa = {!!}
+      ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
+                  →  IProduct {c₁'} A (Obj I) p ai pi )
+      ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g ) 
+     ( Γ : Functor I A ) →   
+     ( lim : Obj A ) 
+     ( proj : (i : Obj I ) → Hom A lim (FObj Γ i) ) → 
+        Limit I Γ lim ( limit-equalizer prod eqa Γ lim proj )
+limit-from prod eqa lim Γ proj = {!!}