Mercurial > hg > Members > kono > Proof > category
changeset 684:5d9d7c2f2718
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Nov 2017 00:09:21 +0900 |
| parents | 88e8a1290dc4 |
| children | f5f582ae20bb |
| files | pullback.agda |
| diffstat | 1 files changed, 7 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Wed Nov 08 00:05:50 2017 +0900 +++ b/pullback.agda Wed Nov 08 00:09:21 2017 +0900 @@ -320,16 +320,16 @@ -- -- -- Γ j = Γ k --- ↑ ^ ↑ --- | | | +-- ↑ ^ ↑ ↑ +-- | | | |proj k -- | |mu u |mu u --- | | | +-- | | | | -- | product of Hom i --- | ↑ ↑ K u = id lim --- | | | +-- | ↑ ↑ | K u = id lim +-- | | | | -- | f|id g|λ u → Γ u d = K j -----------→ K k = d --- proj u | | | | u | --- | | | proj j o e = ε j | | ε k = proj k o e +-- proj j | | | | | u | +-- | | | | proj j o e = ε j | | ε k = proj k o e -- product of Obj i -+ mu u o g o e | | mu u o f o e -- ^ | | -- | e = equalizer f g | |