src/SliceCategories_ch1_6_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
   7 (******************************************************************************)
   8 (* Chapter 1.6.4: Slice Categories                                            *)
   9 (******************************************************************************)
  10
  11 Definition MorphismInTo  `{C:Category}(X:C) := { Y:C & Y~~{C}~~>X }.
  12 Definition MorphismOutOf `{C:Category}(X:C) := { Y:C & X~~{C}~~>Y }.
  13
  14 Definition TriangleAbove `{C:Category}{X:C}(M1 M2:MorphismInTo X) :=
  15    { f:(projT1 M1)~~{C}~~>(projT1 M2) & f >>> (projT2 M2) ~~ (projT2 M1) }.
  16 Definition TriangleBelow `{C:Category}{X:C}(M1 M2:MorphismOutOf X) :=
  17    { f:(projT1 M1)~~{C}~~>(projT1 M2) & (projT2 M1) >>> f ~~ (projT2 M2) }.
  18
  19 Program Instance SliceOver `(C:Category)(X:C) : Category (MorphismInTo X) TriangleAbove :=
  20 { id   := fun y1        => existT _   (id (projT1 y1)) _
  21 ; eqv  := fun a b f g   => eqv    _ _ (projT1 f) (projT1 g)
  22 ; comp := fun _ _ _ f g => existT _   (projT1 f >>> projT1 g) _
  23 }.
  24   Next Obligation.
  25     destruct f. destruct g. destruct H0.  destruct H1. simpl in *. setoid_rewrite <- e.  setoid_rewrite <- e0. apply associativity.
  26     Defined.
  27   Next Obligation.
  28     simpl; setoid_rewrite associativity. reflexivity.
  29     Defined.
  30
  31 Instance SliceOverInclusion `{C:Category}(X:C) : Functor (SliceOver C X) C (fun x => projT1 x) :=
  32   { fmor := fun a b f => projT1 f }.
  33   intros; simpl in H; auto.
  34   intros. destruct a; simpl; auto.
  35   intros. simpl. reflexivity.
  36   Defined.
  37
  38 Program Instance SliceUnder `(C:Category)(X:C) : Category (MorphismOutOf X) TriangleBelow :=
  39 { id   := fun y1        => existT _   (id (projT1 y1)) _
  40 ; eqv  := fun a b f g   => eqv    _ _ (projT1 f) (projT1 g)
  41 ; comp := fun _ _ _ f g => existT _   (projT1 f >>> projT1 g) _
  42 }.
  43   Next Obligation.
  44     destruct f. destruct g. destruct H0.  destruct H1. simpl in *. setoid_rewrite <- associativity.
  45     setoid_rewrite e. auto.
  46     Defined.
  47   Next Obligation.
  48     simpl; setoid_rewrite associativity. reflexivity.
  49     Defined.
  50
  51 Instance SliceUnderInclusion `{C:Category}(X:C) : Functor (SliceUnder C X) C (fun x => projT1 x) :=
  52   { fmor := fun a b f => projT1 f }.
  53   intros; simpl in H; auto.
  54   intros. destruct a; simpl; auto.
  55   intros. simpl. reflexivity.
  56   Defined.