major revision: MonoidalCat is now a subclass of PreMonoidalCat

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

diff --git a/src/SectionRetract_ch2_4.v b/src/SectionRetract_ch2_4.v
index 3eda753..2d4f859 100644 (file)
--- a/src/SectionRetract_ch2_4.v
+++ b/src/SectionRetract_ch2_4.v
@@ -4,6 +4,7 @@ Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
 Require Import ProductCategories_ch1_6_1.
+Require Import NaturalIsomorphisms_ch7_5.
 
 (******************************************************************************)
 (* Chapter 2.4: Sections and Retractions                                      *)
@@ -54,3 +55,13 @@ Instance retract_prod `{C:Category}`{D:Category}{a b:C}{d e:D}(r1:a ⊆ b)(r2:d
 }.
   simpl; split; apply retract_pf.
   Defined.
+
+Structure Retraction `{C:Category} `{D:Category} :=
+{ retraction_section_fobj       : C -> D
+; retraction_section            : Functor C D retraction_section_fobj
+; retraction_retraction_fobj    : D -> C
+; retraction_retraction         : Functor D C retraction_retraction_fobj
+; retraction_composes           : retraction_section >>>> retraction_retraction ≃ functor_id _
+}.
+Implicit Arguments Retraction [ [Ob] [Hom] [Ob0] [Hom0] ].
+Coercion retraction_section : Retraction >-> Functor.