From cc0b4696c2cfc23bdff6ded347478510ccf014c9 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 26 Mar 2011 19:13:15 -0700 Subject: [PATCH 1/1] partial implementation of MonoidalFunctorsCompose --- src/MonoidalCategories_ch7_8.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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. -- 1.7.10.4