partial implementation of MonoidalFunctorsCompose

[coq-categories.git] / src / MonoidalCategories_ch7_8.v

diff --git a/src/MonoidalCategories_ch7_8.v b/src/MonoidalCategories_ch7_8.v
index 8d78f33..e07d035 100644 (file)
--- 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
   }.
   { 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.
 
 
 End MonoidalFunctorsCompose.