Mercurial > hg > Members > kono > Proof > category
diff freyd.agda @ 459:9d24fb809746
freyd trbouled again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Mar 2017 20:22:42 +0900 |
| parents | f526f4b68565 |
| children | 961c236807f1 |
line wrap: on
line diff
--- a/freyd.agda Thu Mar 02 19:04:04 2017 +0900 +++ b/freyd.agda Thu Mar 02 20:22:42 2017 +0900 @@ -58,14 +58,16 @@ F = SFSF SFS FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b FMap← = SFSFMap← SFS - lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (limit-u comp Γ) - lim Γ = isLimit comp Γ + a0 : Obj A + a0 = limit-c comp F + uΓ : ( Γ : Functor A A ) → NTrans A A (K A A (limit-c comp Γ)) Γ + uΓ Γ = {!!} + lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (uΓ Γ) + lim Γ = isLimit comp Γ (uΓ Γ) + u : NTrans A A (K A A a0) F + u = T0 ( lim F ) equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g equ f g = Complete.isEqualizer comp f g - a0 : Obj A - a0 = limit-c comp F - u : NTrans A A (K A A a0) F - u = limit-u comp F ep : {a b : Obj A} → {f g : Hom A a b} → Obj A ep {a} {b} {f} {g} = equalizer-p comp f g ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a