Mercurial > hg > Members > kono > Proof > category
changeset 462:e618db534987
clean up fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 Mar 2017 10:54:26 +0900 |
| parents | 8436a018f88a |
| children | 4c686e19db60 |
| files | limit-to.agda |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Sat Mar 04 10:43:17 2017 +0900 +++ b/limit-to.agda Sat Mar 04 10:54:26 2017 +0900 @@ -71,28 +71,28 @@ id1 A b o id1 A b ∎ distr1 {t0} {t0} {t1} { id-t0 } { arrow-f } = let open ≈-Reasoning A in begin - fmap (comp arrow-f id-t0) + fmap (T [ arrow-f o id-t0 ] ) ≈⟨⟩ fmap arrow-f ≈↑⟨ idR ⟩ fmap arrow-f o id1 A a ∎ distr1 {t0} {t0} {t1} { id-t0 } { arrow-g } = let open ≈-Reasoning A in begin - fmap (comp arrow-g id-t0) + fmap (T [ arrow-g o id-t0 ] ) ≈⟨⟩ fmap arrow-g ≈↑⟨ idR ⟩ fmap arrow-g o id1 A a ∎ distr1 {t0} {t1} {t1} { arrow-f } { id-t1 } = let open ≈-Reasoning A in begin - fmap (comp id-t1 arrow-f) + fmap (T [ id-t1 o arrow-f ] ) ≈⟨⟩ fmap arrow-f ≈↑⟨ idL ⟩ id1 A b o fmap arrow-f ∎ distr1 {t0} {t1} {t1} { arrow-g } { id-t1 } = let open ≈-Reasoning A in begin - fmap (comp id-t1 arrow-g) + fmap (T [ id-t1 o arrow-g ] ) ≈⟨⟩ fmap arrow-g ≈↑⟨ idL ⟩