1 Generalizable All Variables.
2 Require Import Preamble.
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.
8 (******************************************************************************)
9 (* Chapter 2.4: Sections and Retractions *)
10 (******************************************************************************)
12 (* FIXME: do sections as well *)
14 Class RetractsInto `{C:Category} (A B:C) :=
15 { retract_embed : A~~{C}~~>B
16 ; retract_project : B~~{C}~~>A
17 ; retract_pf : retract_embed >>> retract_project ~~ id _
19 Notation "A ⊆ B" := (@RetractsInto _ _ _ A B) (at level 100).
20 Implicit Arguments retract_embed [ Ob Hom C A B ].
21 Implicit Arguments retract_project [ Ob Hom C A B ].
24 Instance FunctorsPreserveRetracts `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj){a b:C}(r:a ⊆ b) : ((Fobj a) ⊆ (Fobj b)) :=
25 { retract_embed := F \ (retract_embed r)
26 ; retract_project := F \ (retract_project r)
28 setoid_rewrite (fmor_preserves_comp F).
29 setoid_rewrite retract_pf.
30 apply fmor_preserves_id.
33 Instance iso_retract `{CX:Category}(a b:CX)(i:a ≅ b) : (a ⊆ b) :=
34 { retract_embed := iso_forward i
35 ; retract_project := iso_backward i
40 Instance retract_comp `{CX:Category}(a b c:CX)(r1:a ⊆ b)(r2:b ⊆ c) : (a ⊆ c) :=
41 { retract_embed := (retract_embed r1) >>> (retract_embed r2)
42 ; retract_project := (retract_project r2) >>> (retract_project r1)
44 setoid_rewrite juggle3.
45 setoid_rewrite retract_pf.
46 setoid_rewrite right_identity.
50 Instance retract_prod `{C:Category}`{D:Category}{a b:C}{d e:D}(r1:a ⊆ b)(r2:d ⊆ e)
51 : @RetractsInto _ _ (C ×× D) (pair_obj a d) (pair_obj b e) :=
52 { retract_embed := pair_mor (pair_obj a d) (pair_obj b e) (retract_embed r1) (retract_embed r2)
53 ; retract_project := pair_mor (pair_obj b e) (pair_obj a d) (retract_project r1) (retract_project r2)
55 simpl; split; apply retract_pf.