src/SectionRetract_ch2_4.v

   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.
   7
   8 (******************************************************************************)
   9 (* Chapter 2.4: Sections and Retractions                                      *)
  10 (******************************************************************************)
  11
  12 (* FIXME: do sections as well *)
  13
  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 _
  18 }.
  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 ].
  22
  23 (* Remark 2.14 *)
  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)
  27 }.
  28   setoid_rewrite (fmor_preserves_comp F).
  29   setoid_rewrite retract_pf.
  30   apply fmor_preserves_id.
  31   Defined.
  32
  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
  36 }.
  37   apply (iso_comp1 i).
  38   Defined.
  39
  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)
  43 }.
  44   setoid_rewrite juggle3.
  45   setoid_rewrite retract_pf.
  46   setoid_rewrite right_identity.
  47   apply retract_pf.
  48   Defined.
  49
  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)
  54 }.
  55   simpl; split; apply retract_pf.
  56   Defined.