# HG changeset patch # User Shinji KONO # Date 1510067361 -32400 # Node ID 5d9d7c2f2718d7b08096c590814d5fecf09b57d4 # Parent 88e8a1290dc4ac9525b1f29234018472a44d9a98 ... diff -r 88e8a1290dc4 -r 5d9d7c2f2718 pullback.agda --- 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 | |