X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FSectionRetract_ch2_4.v;h=3053462ef9fd8d877da7c4d66fb5a31a740f531c;hp=2d4f859333c61f23c09ca1be7f50acbdc0ea7bc3;hb=1104780d775bf36ff9f44ab287c22604ab47f0b5;hpb=27ffdd2265eb1c15acc62970f49d25a07bcadb05

diff --git a/src/SectionRetract_ch2_4.v b/src/SectionRetract_ch2_4.v
index 2d4f859..3053462 100644
--- a/src/SectionRetract_ch2_4.v
+++ b/src/SectionRetract_ch2_4.v
@@ -1,5 +1,5 @@
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
@@ -56,12 +56,12 @@ 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} :=
+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.