Mercurial > hg > Members > kono > Proof > category
changeset 277:21ef5ba54458
2 yellow remains
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 23 Sep 2013 01:10:48 +0900 |
| parents | 70a919162e27 |
| children | 9fafe4a53f89 |
| files | pullback.agda |
| diffstat | 1 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Mon Sep 23 00:14:54 2013 +0900 +++ b/pullback.agda Mon Sep 23 01:10:48 2013 +0900 @@ -244,11 +244,11 @@ -- U = λ b → A0 (lim b {a0 b} {t0 b} -- ε = λ b → T0 ( lim b {a0 b} {t0 b} ) -limit2adjoint : +limit2couniv : ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 ) → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K I (a0 b) ) b ) → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) ) -limit2adjoint lim a0 t0 = record { -- F U ε +limit2couniv lim a0 t0 = record { -- F U ε _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η iscoUniversalMapping = record { couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; @@ -316,7 +316,7 @@ → ( ∀ { 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 ε )) ⟩ + ≈↑⟨ car ( fcong U εf=t ) ⟩ (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