Mercurial > hg > Members > kono > Proof > category
diff equalizer.agda @ 440:ff36c500962e
fix limit
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 30 Aug 2016 14:22:47 +0900 |
| parents | d6a6dd305da2 |
| children | f526f4b68565 |
line wrap: on
line diff
--- a/equalizer.agda Tue Aug 30 01:40:56 2016 +0900 +++ b/equalizer.agda Tue Aug 30 14:22:47 2016 +0900 @@ -247,7 +247,7 @@ → Burroni A {c} {a} {b} f g e lemma-equ1 {a} {b} {c} f g e eqa = record { α = λ {a} {b} {c} f g e → equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a - γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) + γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d δ = λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f); -- Hom A a c cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ; @@ -256,7 +256,7 @@ b1 = fe=ge (eqa {a} {b} {c} f g {e}) ; b2 = lemma-b2 ; b3 = lemma-b3 ; - b4 = lemma-b4 + b4 = lemma-b4 } where -- -- e eqa f g f