Mercurial > hg > Members > kono > Proof > category

changeset 276:70a919162e27

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
yellow remains ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 00:14:54 +0900
parents 62e84bea7b29
children 21ef5ba54458
files pullback.agda
diffstat 1 files changed, 15 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sun Sep 22 23:49:52 2013 +0900
+++ b/pullback.agda	Mon Sep 23 00:14:54 2013 +0900
@@ -316,7 +316,21 @@
          → ( ∀ { 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
-        ≈⟨ {!!} ⟩
+        ≈⟨ car ( fcong U ( nat ε )) ⟩
+            (FMap U ( A ^ I [ TMap ε Γ o FMap ( KI I) f ] )) o TMap η a 
+        ≈⟨ car ( distr U ) ⟩
+            (FMap U (TMap ε Γ) o   FMap U ( FMap ( KI I) f) ) o TMap η a 
+        ≈⟨⟩
+            (FMap U (TMap ε Γ) o   FMap (U ○ KI I) f ) o TMap η a 
+        ≈↑⟨ assoc ⟩
+            FMap U (TMap ε Γ) o  ( FMap (U ○ KI I) f o TMap η a ) 
+        ≈⟨ cdr ( nat η )  ⟩
+            FMap U (TMap ε Γ) o ( TMap η (FObj U Γ) o  f )
+        ≈⟨ assoc ⟩
+            (FMap U (TMap ε Γ) o TMap η (FObj U Γ)) o  f
+        ≈⟨  car ( IsAdjunction.adjoint1 ( isAdjunction adj)) ⟩
+            id1 A (FObj U Γ) o  f
+        ≈⟨ idL ⟩
             f
         ∎