X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FMonoidalCategories_ch7_8.v;h=e07d03501bcefd716498fabea645a344a26f116e;hp=8d78f33a85b7de3c9ebcca22e74d6fd5bdd37a99;hb=cc0b4696c2cfc23bdff6ded347478510ccf014c9;hpb=ff268c0e8d10a75c5f82b0ae69feda0ec36faa4b;ds=sidebyside

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 8d78f33..e07d035 100644
--- a/src/MonoidalCategories_ch7_8.v
+++ b/src/MonoidalCategories_ch7_8.v
@@ -436,7 +436,10 @@ Section MonoidalFunctorsCompose.
   { mf_id        := id_comp         (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
   ; mf_coherence := mf_compose_coherence
   }.
-  Admitted.
+  admit.
+  admit.
+  admit.
+  Defined.
 
 End MonoidalFunctorsCompose.