From add4d471e2d188c62bddbdaa21380ee5904bdedc Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 5 Apr 2011 06:32:20 +0000 Subject: [PATCH] rename Retraction to RetractionOfCategories --- src/SectionRetract_ch2_4.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/SectionRetract_ch2_4.v b/src/SectionRetract_ch2_4.v index 2d4f859..17ab24a 100644 --- a/src/SectionRetract_ch2_4.v +++ b/src/SectionRetract_ch2_4.v @@ -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. -- 1.7.10.4