Mercurial > hg > Members > kono > Proof > category

changeset 295:26e8f0227ebd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit equation done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 25 Sep 2013 20:24:39 +0900
parents db4ecbdbf9e9
children bba60d843462
files pullback.agda
diffstat 1 files changed, 33 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Wed Sep 25 19:54:35 2013 +0900
+++ b/pullback.agda	Wed Sep 25 20:24:39 2013 +0900
@@ -512,8 +512,39 @@
          limit1 a t = A [ FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a ]
          t0f=t1 :  {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {i : Obj I} →
                 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ]
-         t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in {!!}
+         t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in  begin
+                 TMap ta i o limit1 a t 
+               ≈⟨⟩
+                  FMap U ( TMap tb i )  o ( FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a  )
+               ≈⟨ assoc ⟩
+                  ( FMap U ( TMap tb i )  o  FMap U (limit limitb (FObj F a) (tF a t ))) o TMap η a  
+               ≈↑⟨ car ( distr U ) ⟩
+                  FMap U ( B [ TMap tb i  o limit limitb (FObj F a) (tF a t ) ] ) o TMap η a  
+               ≈⟨ car ( fcong U ( t0f=t limitb ) ) ⟩
+                  FMap U (TMap (tF a t) i) o TMap η a  
+               ≈⟨⟩
+                  FMap U ( B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ] ) o TMap η a  
+               ≈⟨ car ( distr U ) ⟩
+                  ( FMap U ( TMap ε (FObj Γ i))  o FMap U ( FMap F (TMap t i) )) o TMap η a  
+               ≈↑⟨ assoc ⟩
+                   FMap U ( TMap ε (FObj Γ i) ) o ( FMap U ( FMap F (TMap t i) ) o TMap η a   )
+               ≈⟨ cdr ( nat η ) ⟩
+                    FMap U (TMap ε (FObj Γ i)) o (  TMap η (FObj U (FObj Γ i)) o FMap (identityFunctor {_} {_} {_} {A}) (TMap t i) )
+               ≈⟨ assoc ⟩
+                    ( FMap U (TMap ε (FObj Γ i)) o   TMap η (FObj U (FObj Γ i))) o TMap t i
+               ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj ) ) ⟩
+                 id1 A (FObj (U ○ Γ) i) o TMap t i
+               ≈⟨ idL ⟩
+                 TMap t i
+               ∎
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {f : Hom A a (FObj U lim)} 
                 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) →
                 A [ limit1 a t ≈ f ]
-         limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in {!!}
+         limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in  begin
+                 limit1 a t
+               ≈⟨⟩
+                 FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a  
+               ≈⟨ {!!} ⟩
+                 f
+               ∎
+