retract.v

   1 Require Import Morphisms.
   2 Require Import RelationClasses.
   3 Require Import Equivalence.
   4 Require Import Setoid.
   5
   6 (* Eelis *)
   7 Require Import interfaces.abstract_algebra interfaces.functors theory.categories.
   8 (* me *)
   9 Require Import square.
  10
  11 Set Automatic Introduction.
  12
  13 Section Retract.
  14
  15 Context `{Category C}.
  16
  17 Class Retract {a b a' b': C} (i: a'⟶a) (p: a⟶a') (i':b'⟶b) (p':b⟶b') (f: a⟶b) (g: a'⟶b') := retract {
  18   top : p ◎ i = cat_id;
  19   bottom : p' ◎ i' = cat_id;
  20   sq_l : Square g f i i';
  21   sq_r : Square f g p p'
  22 }.
  23
  24 Section stuff_1.
  25 Context (a b:C) (i:a ⟶ b) (p: b⟶a) (HH:p ◎ i = cat_id).
  26 Program Instance: Retract i p cat_id cat_id p cat_id .
  27 Next Obligation. apply id_l. Qed.
  28 Next Obligation. unfold Square; rewrite HH; apply id_l. Qed.
  29 Next Obligation. red; reflexivity. Qed.
  30
  31 Program Instance: Retract cat_id cat_id i p i cat_id.
  32 Next Obligation. apply id_l. Qed.
  33 Next Obligation. red; reflexivity. Qed.
  34 Next Obligation. red. rewrite HH; symmetry; apply id_l. Qed.
  35
  36 Context (c d:C) (j:c ⟶ d) (q: d⟶c) (II:q ◎ j = cat_id).
  37 Context (f:a⟶c).
  38 Program Instance: Retract i p j q (j ◎ f ◎ p) f.
  39 Next Obligation. red. rewrite <- comp_assoc, HH, id_r; reflexivity. Qed.
  40 Next Obligation. red. rewrite comp_assoc, comp_assoc, II, id_l; reflexivity. Qed.
  41 End stuff_1.
  42
  43 Section stuff_2.
  44 Context (a b:C) (i:a ⟶ b) (p: b⟶a) (HH:p ◎ i = cat_id).
  45 Context (c:C) (j:c ⟶ b) (q: b⟶c) (II:q ◎ j = cat_id).
  46 Program Instance: Retract i p j q cat_id (q ◎ i).
  47 Next Obligation. red. rewrite id_l, comp_assoc. admit. Qed.
  48 Next Obligation. red. rewrite id_r. admit. Qed.
  49 End stuff_2.
  50
  51 Section stuff_3.
  52 Context (a b x y c:C) (i:a ⟶ b) (p: x⟶y) (f:a⟶x) (g:b⟶y).
  53 Context (Sq: Square i p f g).
  54 Context (h:b⟶x) (UT:h◎i = f) (LT:p◎h = g).
  55 Context (j:b⟶c) (q:c⟶x) (F:q◎j=h).
  56 Context (q':x⟶c) (L:q◎q'=cat_id) (LL:q'◎f = j◎i).
  57 (*Context (j':c⟶b) (L:j◎j'=cat_id) (LL:q'◎f = j◎i).*)
  58 Program Instance: Retract cat_id cat_id q' q (j◎i) f.
  59 Next Obligation. apply id_l. Qed.
  60 Next Obligation. red. rewrite id_r. apply LL. Qed.
  61 Next Obligation. red. rewrite id_r, comp_assoc. rewrite F. apply UT. Qed.
  62
  63 End stuff_3.
  64
  65 End Retract.