cross.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.
   8 (* me *)
   9
  10 Section Cross.
  11  Context `(Category L) `(Category R).
  12
  13 Inductive Object :=
  14 | inl : L -> Object
  15 | inr : R -> Object
  16 | cross
  17 .
  18
  19 Definition Arrow (x y: Object) : Type := match x, y with
  20     | inl l, inl r => l ⟶ r
  21     | inr l, inr r => l ⟶ r
  22     | inl _, _ => unit
  23     | _, inr _ => unit
  24     | cross, cross => unit
  25     | _, _ => Empty_set
  26 end.
  27
  28 Global Instance: Arrows Object := Arrow.
  29 Hint Extern 4 (Arrows Object) => exact Arrow: typclasses_instance.
  30
  31 Section contents.
  32 Section more_arrows. Context (x y: Object).
  33     Global Instance e: Equiv (x ⟶ y) :=
  34       match x, y with
  35         | inl l, inl r => fun f g: l ⟶ r => f = g
  36         | inr l, inr r => fun f g: l ⟶ r => f = g
  37         | _, _ => fun _ _ => True
  38       end.
  39
  40     Let e_refl: Reflexive e.
  41     Proof.
  42       intro f.
  43       unfold e.
  44       destruct x, y; reflexivity.
  45     Qed.
  46
  47     Let e_sym: Symmetric e.
  48     Proof.
  49       clear e_refl.
  50       unfold e.
  51       intros f g.
  52       destruct x, y; try symmetry; trivial.
  53     Qed.
  54
  55     Let e_trans: Transitive e.
  56     Proof.
  57       clear e_refl e_sym.
  58       intros f g h . unfold e.
  59       destruct x, y; try transitivity g; trivial.
  60     Qed.
  61     Instance: Equivalence e.
  62     Global Instance: Setoid (x⟶y).
  63   End more_arrows.
  64
  65     Global Instance: CatId Object.
  66     Proof.
  67       intro x; destruct x; compute; exact cat_id || exact tt.
  68     Defined.
  69
  70     Global Instance: CatComp Object.
  71       intros x y z; destruct x, y, z; compute; trivial;
  72         try contradiction; apply comp.
  73     Defined.
  74
  75     Let id_l' (x y: Object) (f: x ⟶ y): cat_id ◎ f = f.
  76     Proof.
  77       destruct x, y; compute; trivial; apply id_l.
  78     Qed.
  79     Let id_r' (x y: Object) (f: x ⟶ y): f ◎ cat_id = f.
  80     Proof.
  81       destruct x, y; compute; trivial; apply id_r.
  82     Qed.
  83
  84   Section comp_assoc.
  85     Context (w x y z: Object) (a: w ⟶ x) (b: x ⟶ y) (c: y ⟶ z).
  86     Lemma comp_assoc': c ◎ (b ◎ a) = (c ◎ b) ◎ a.
  87     Proof.
  88       destruct w, x, y, z; compute; trivial; try contradiction; apply comp_assoc.
  89     Qed.
  90   End comp_assoc.
  91
  92   Global Instance: forall x y z: Object, Proper (equiv ==> equiv ==> equiv)
  93     ((◎) : (y ⟶ z) -> (x ⟶ y) -> (x ⟶ z)).
  94   Proof.
  95     intros x y z; destruct x, y, z; compute; trivial; try contradiction; [apply H0 | apply H2].
  96   Qed.
  97
  98   Global Instance: Category Object := { comp_assoc := comp_assoc'; id_l := id_l'; id_r := id_r'}.
  99
 100 End contents.
 101
 102 End Cross.