Mercurial > hg > Members > kono > Proof > category
changeset 269:6056a995964b
adjoint form limit
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 22 Sep 2013 18:48:12 +0900 |
| parents | 2ff44ee3cb32 |
| children | 8ba03259a177 |
| files | pullback.agda |
| diffstat | 1 files changed, 13 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Sun Sep 22 18:05:09 2013 +0900 +++ b/pullback.agda Sun Sep 22 18:48:12 2013 +0900 @@ -232,8 +232,17 @@ open import Function -limit2adjoint : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) - ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) - ( lim : Limit I Γ a0 t0 ) → coUniversalMapping A ( A ^ I ) (KI I) ({!!}) ({!!}) -limit2adjoint = {!!} +lim-ε : ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) + ( lim : Limit I Γ a0 t0 ) → (b : Obj ( A ^ I )) → NTrans I A (FObj (KI I) a0) b +lim-ε a0 t0 lim b = {!!} +limit2adjoint : ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) + ( lim : Limit I Γ a0 t0 ) → coUniversalMapping A ( A ^ I ) (KI I) (λ b → a0 ) (lim-ε a0 t0 lim) +limit2adjoint a0 t0 lim = record { + _*' = λ {b} {a} k → limit lim a ? ; + iscoUniversalMapping = record { + couniversalMapping = {!!} ; + couniquness = {!!} + } + } +