Mercurial > hg > Members > kono > Proof > category

changeset 275:62e84bea7b29

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 23:49:52 +0900
parents 1b651faa2391
children 70a919162e27
files pullback.agda
diffstat 1 files changed, 18 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sun Sep 22 22:43:25 2013 +0900
+++ b/pullback.agda	Sun Sep 22 23:49:52 2013 +0900
@@ -274,6 +274,9 @@
         ∎
 
 open import Category.Cat
+
+open Adjunction
+
 adjoint2limit : 
      ( U : Functor (A ^ I) A ) ( η :  NTrans A A identityFunctor ( U ○  (KI I) ) )
      ( ε :   NTrans (A ^ I) (A ^ I)  ( (KI I) ○  U ) identityFunctor )
@@ -292,7 +295,21 @@
             TMap (TMap ε Γ) i o limit1 a t
         ≈⟨⟩
             TMap (TMap ε Γ) i o ( FMap U t  o TMap η a )
-        ≈⟨ {!!} ⟩
+        ≈⟨ assoc  ⟩
+            (TMap (TMap ε Γ) i o  FMap U t ) o TMap η a 
+        ≈⟨ car (nat ε)  ⟩
+           TMap (FMap (KI I) (TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o FMap U (FMap (KI I) (TMap t i)))) i o TMap η a
+        ≈⟨ car (distr (KI I)) ⟩
+            (TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o   FMap (U ○ KI I) (TMap t i)) o TMap η a 
+        ≈↑⟨ assoc  ⟩
+            TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o (  FMap (U ○ KI I) (TMap t i) o TMap η a )
+        ≈⟨ cdr ( nat η ) ⟩
+            TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o ((TMap (FMap (KI I) (TMap η (FObj Γ i))) i) o TMap t i )
+        ≈⟨ assoc ⟩
+            ( TMap (TMap ε (FObj (KI I) (FObj Γ i))) i o (TMap (FMap (KI I) (TMap η (FObj Γ i))) i)) o TMap t i
+        ≈⟨  car ( IsAdjunction.adjoint2 ( isAdjunction adj)) ⟩
+            id1 A  (FObj Γ i) o TMap t i
+        ≈⟨ idL ⟩
             TMap t i
         ∎
      limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (FObj U Γ)}