Mercurial > hg > Members > kono > Proof > category
changeset 297:537570f6a44f
limit preservation proved.
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Sep 2013 21:12:29 +0900 |
| parents | bba60d843462 |
| children | 61669ac03e7d |
| files | pullback.agda |
| diffstat | 1 files changed, 21 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Wed Sep 25 21:03:15 2013 +0900 +++ b/pullback.agda Wed Sep 25 21:12:29 2013 +0900 @@ -547,13 +547,31 @@ 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 + ≈⟨ car (distr U ) ⟩ + ( (FMap U (TMap ε lim)) o (FMap U ( FMap F f )) ) o TMap η a + ≈⟨ sym assoc ⟩ + (FMap U (TMap ε lim)) o ((FMap U ( FMap F f )) o TMap η a ) + ≈⟨ cdr (nat η) ⟩ + (FMap U (TMap ε lim)) o ((TMap η (FObj U lim )) o f ) + ≈⟨ assoc ⟩ + ((FMap U (TMap ε lim)) o (TMap η (FObj U lim))) o f + ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj)) ⟩ + id (FObj U lim) o f + ≈⟨ idL ⟩ + 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) - ≈⟨ {!!} ⟩ + ≈⟨ assoc ⟩ + ( TMap tb i o TMap ε lim ) o FMap F f + ≈⟨ car ( nat ε ) ⟩ + ( TMap ε (FObj Γ i) o FMap F ( FMap U ( TMap tb i ))) o FMap F f + ≈↑⟨ assoc ⟩ + TMap ε (FObj Γ i) o ( FMap F ( FMap U ( TMap tb i )) o FMap F f ) + ≈↑⟨ cdr ( distr F ) ⟩ + TMap ε (FObj Γ i) o FMap F ( A [ FMap U ( TMap tb i ) o f ] ) + ≈⟨ cdr ( fcong F (lim=t {i}) ) ⟩ TMap ε (FObj Γ i) o FMap F (TMap t i) ≈⟨⟩ TMap (tF a t) i