X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FNaturalIsomorphisms_ch7_5.v;h=90ce3260e43d16a4c6b28d9a038b3ca815cf3c75;hp=33716718e59171d6968ee7521be299a029e4f778;hb=107e8eb4dc6e893c3dd93535c5343eba204659a8;hpb=06467b1762fe54767eb1d64e7b7f1798eea8cc27

diff --git a/src/NaturalIsomorphisms_ch7_5.v b/src/NaturalIsomorphisms_ch7_5.v
index 3371671..90ce326 100644
--- a/src/NaturalIsomorphisms_ch7_5.v
+++ b/src/NaturalIsomorphisms_ch7_5.v
@@ -251,3 +251,13 @@ Section ni_prod_comp.
     split; reflexivity.
     Defined.
 End ni_prod_comp.
+
+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.