Mercurial > hg > Members > kono > Proof > category

changeset 279:8df8e74e6316

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit and prod/equalizer
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 03:31:24 +0900
parents 9fafe4a53f89
children 7ae58263d45b
files pullback.agda
diffstat 1 files changed, 23 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 02:39:57 2013 +0900
+++ b/pullback.agda	Mon Sep 23 03:31:24 2013 +0900
@@ -234,8 +234,6 @@
         ∎
 
 
-open import Function
-
 ---------
 --
 -- limit gives co universal mapping ( i.e. adjunction )
@@ -279,28 +277,28 @@
 open coUniversalMapping
  
 univ2limit : 
-     ( U : Functor (A ^ I) A ) 
-     ( ε :   NTrans (A ^ I) (A ^ I)  ( (KI I) ○  U ) identityFunctor )
-     ( univ :  coUniversalMapping A (A ^ I) (KI I) (FObj U) (TMap ε) ) →
-     ( Γ : Functor I A ) →   Limit I Γ (FObj U Γ) (TMap ε Γ)
+     ( U : Obj (A ^ I ) → Obj A ) 
+     ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K I (U b)) b )
+     ( univ :  coUniversalMapping A (A ^ I) (KI I) U (ε) ) →
+     ( Γ : Functor I A ) →   Limit I Γ (U Γ) (ε Γ)
 univ2limit U ε univ Γ = record {
      limit = λ a t → limit1 a t ;
      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
-     limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a (FObj U Γ)
-     limit1 a t = _*' univ t 
-     t0f=t1 :   {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} →
-                A [ A [ TMap (TMap ε Γ) i o limit1 a t ] ≈ TMap t i ]
+     limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a (U Γ)
+     limit1 a t = _*' univ {_} {a} t 
+     t0f=t1 :   {a : Obj A} {t : NTrans I A (K I a) Γ}  {i : Obj I} →
+                A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
      t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
-            TMap (TMap ε Γ) i o limit1 a t
+            TMap (ε Γ) i o limit1 a t
         ≈⟨⟩
-            TMap (TMap ε Γ) i o _*' univ t
-        ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) ⟩
+            TMap (ε Γ) i o _*' univ {{!!}} {{!!}} t
+        ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {{!!}} {{!!}} {{!!}}  ⟩
             TMap t i
         ∎
-     limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (FObj U Γ)} 
-         → ( ∀ { i : Obj I } → A [ A [ TMap  (TMap ε Γ) i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
+     limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (U Γ)} 
+         → ( ∀ { i : Obj I } → A [ A [ TMap  (ε Γ) i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
      limit-uniqueness1 {a} {t} {f} εf=t = let  open ≈-Reasoning (A) in begin
             _*' univ t
         ≈⟨  ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t  ⟩
@@ -310,3 +308,13 @@
 
 
  
+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 = ?