Mercurial > hg > Members > kono > Proof > category
changeset 296:bba60d843462
lemma1 will be proved
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Sep 2013 21:03:15 +0900 |
| parents | 26e8f0227ebd |
| children | 537570f6a44f |
| files | pullback.agda |
| diffstat | 1 files changed, 14 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Wed Sep 25 20:24:39 2013 +0900 +++ b/pullback.agda Wed Sep 25 21:03:15 2013 +0900 @@ -537,6 +537,7 @@ ≈⟨ idL ⟩ TMap t i ∎ + -- ta = TMap (Functor*Nat I A U tb) , FMap U ( TMap tb i ) o f ≈ 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 ] @@ -544,7 +545,19 @@ limit1 a t ≈⟨⟩ FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a + ≈⟨ car ( fcong U (limit-uniqueness limitb ( λ {i} → lemma1 i) )) ⟩ + FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a ≈⟨ {!!} ⟩ f - ∎ + ∎ where + lemma1 : (i : Obj I) → B [ B [ TMap tb i o B [ TMap ε lim o FMap F f ] ] ≈ TMap (tF a t) i ] + lemma1 i = let open ≈-Reasoning (B) in begin + TMap tb i o (TMap ε lim o FMap F f) + ≈⟨ {!!} ⟩ + TMap ε (FObj Γ i) o FMap F (TMap t i) + ≈⟨⟩ + TMap (tF a t) i + ∎ + +