Mercurial > hg > Members > kono > Proof > category

changeset 272:5f2b8a5cc115

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adjunction to limit
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 21:27:03 +0900
parents 28278175d696
children fae4bb967d76
files pullback.agda
diffstat 1 files changed, 31 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sun Sep 22 20:40:17 2013 +0900
+++ b/pullback.agda	Sun Sep 22 21:27:03 2013 +0900
@@ -236,6 +236,14 @@
 
 open import Function
 
+---------
+--
+-- limit gives co universal mapping ( i.e. adjunction )
+--
+--     F = KI I : Functor A (A ^ I)
+--     U = λ b → A0 (lim b {a0 b} {t0 b} 
+--     ε = λ b → T0 ( lim b {a0 b} {t0 b} ) 
+
 limit2adjoint : 
      ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 )
      → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 :  ( b : Functor I A ) → NTrans I A ( K I (a0 b) ) b )
@@ -257,14 +265,34 @@
             TMap f i  -- i comes from   ∀{i} → B [ TMap f i  ≈  TMap g i  ]
         ∎
    couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} →
-        ( ∀ { i : Obj I } →
-        A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i  o TMap ( FMap (KI I) g) i  ] ≈ TMap f i ] ) → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ]
+        ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i  o TMap ( FMap (KI I) g) i  ] ≈ TMap f i ] ) 
+         → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ]
    couniquness2 {b} {a} {f} {g} lim-g=f  =  let  open ≈-Reasoning (A) in begin
             limit (lim b {a0 b} {t0 b} ) a f
         ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) lim-g=f ⟩
             g
         ∎
 
+open import Category.Cat
+
+adjoint2limit : 
+     ( U : Functor (A ^ I) A ) ( η :  NTrans A A identityFunctor ( U ○  (KI I) ) )
+     ( ε :   NTrans (A ^ I) (A ^ I)  ( (KI I) ○  U ) identityFunctor )
+     ( adj : Adjunction A (A ^ I) U (KI I) η ε ) →
+     ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 
+adjoint2limit U η ε adj Γ {a0} {t0} = 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 ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
+     limit1 a t = {!!}
+     t0f=t1 :  { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } →
+         A [ A [ TMap t0 i o  limit1 a t ]  ≈ TMap t i ]
+     t0f=t1 = {!!}
+     limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
+         A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
+     limit-uniqueness1 = {!!}
 
 
-
+