1 Generalizable All Variables.
2 Require Import Notations.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
5 Require Import Isomorphisms_ch1_5.
6 Require Import ProductCategories_ch1_6_1.
7 Require Import NaturalIsomorphisms_ch7_5.
9 (******************************************************************************)
10 (* Chapter 2.4: Sections and Retractions *)
11 (******************************************************************************)
13 (* FIXME: do sections as well *)
15 Class RetractsInto `{C:Category} (A B:C) :=
16 { retract_embed : A~~{C}~~>B
17 ; retract_project : B~~{C}~~>A
18 ; retract_pf : retract_embed >>> retract_project ~~ id _
20 Notation "A ⊆ B" := (@RetractsInto _ _ _ A B) (at level 100).
21 Implicit Arguments retract_embed [ Ob Hom C A B ].
22 Implicit Arguments retract_project [ Ob Hom C A B ].
25 Instance FunctorsPreserveRetracts `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj){a b:C}(r:a ⊆ b) : ((Fobj a) ⊆ (Fobj b)) :=
26 { retract_embed := F \ (retract_embed r)
27 ; retract_project := F \ (retract_project r)
29 setoid_rewrite (fmor_preserves_comp F).
30 setoid_rewrite retract_pf.
31 apply fmor_preserves_id.
34 Instance iso_retract `{CX:Category}(a b:CX)(i:a ≅ b) : (a ⊆ b) :=
35 { retract_embed := iso_forward i
36 ; retract_project := iso_backward i
41 Instance retract_comp `{CX:Category}(a b c:CX)(r1:a ⊆ b)(r2:b ⊆ c) : (a ⊆ c) :=
42 { retract_embed := (retract_embed r1) >>> (retract_embed r2)
43 ; retract_project := (retract_project r2) >>> (retract_project r1)
45 setoid_rewrite juggle3.
46 setoid_rewrite retract_pf.
47 setoid_rewrite right_identity.
51 Instance retract_prod `{C:Category}`{D:Category}{a b:C}{d e:D}(r1:a ⊆ b)(r2:d ⊆ e)
52 : @RetractsInto _ _ (C ×× D) (pair_obj a d) (pair_obj b e) :=
53 { retract_embed := pair_mor (pair_obj a d) (pair_obj b e) (retract_embed r1) (retract_embed r2)
54 ; retract_project := pair_mor (pair_obj b e) (pair_obj a d) (retract_project r1) (retract_project r2)
56 simpl; split; apply retract_pf.
59 Structure RetractionOfCategories `{C:Category} `{D:Category} :=
60 { retraction_section_fobj : C -> D
61 ; retraction_section : Functor C D retraction_section_fobj
62 ; retraction_retraction_fobj : D -> C
63 ; retraction_retraction : Functor D C retraction_retraction_fobj
64 ; retraction_composes : retraction_section >>>> retraction_retraction ≃ functor_id _
66 Implicit Arguments RetractionOfCategories [ [Ob] [Hom] [Ob0] [Hom0] ].
67 Coercion retraction_section : RetractionOfCategories >-> Functor.