Mercurial > hg > Members > kono > Proof > category

changeset 274:1b651faa2391

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adjoint2limit problems are written
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 22:43:25 +0900
parents fae4bb967d76
children 62e84bea7b29
files pullback.agda
diffstat 1 files changed, 24 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sun Sep 22 21:35:20 2013 +0900
+++ b/pullback.agda	Sun Sep 22 22:43:25 2013 +0900
@@ -248,8 +248,8 @@
      ( 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 )
      →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) )  ( λ b → T0 ( lim b {a0 b} {t0 b} ) )
-limit2adjoint lim a0 t0 = record {
-       _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ;
+limit2adjoint lim a0 t0 = record {  -- F             U                            ε
+       _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η
        iscoUniversalMapping = record {
            couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; 
            couniquness = couniquness2
@@ -274,25 +274,35 @@
         ∎
 
 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 {
+     ( Γ : Functor I A ) →   Limit I Γ (FObj U Γ) (TMap ε Γ)
+adjoint2limit U η ε adj Γ = 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
-     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 = {!!}
+     limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a (FObj U Γ)
+     limit1 a t = A [ FMap U t o TMap η a ] 
+     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 ]
+     t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
+            TMap (TMap ε Γ) i o limit1 a t
+        ≈⟨⟩
+            TMap (TMap ε Γ) i o ( FMap U t  o TMap η a )
+        ≈⟨ {!!} ⟩
+            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} {t} {f} εf=t = let  open ≈-Reasoning (A) in begin
+            FMap U t  o TMap η a
+        ≈⟨ {!!} ⟩
+            f
+        ∎
+