Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
simpl; split; apply retract_pf.
Defined.
-Structure Retraction `{C:Category} `{D:Category} :=
+Structure RetractionOfCategories `{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.
+Implicit Arguments RetractionOfCategories [ [Ob] [Hom] [Ob0] [Hom0] ].
+Coercion retraction_section : RetractionOfCategories >-> Functor.