# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1488592466 -32400
# Node ID e618db53498728abe0164b37063072e5a831d8fa
# Parent  8436a018f88aed51403771120bcfc1b88dfd6445
clean up fix

diff -r 8436a018f88a -r e618db534987 limit-to.agda
--- 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 ⟩