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.
7 (******************************************************************************)
8 (* Chapter 1.6.4: Slice Categories *)
9 (******************************************************************************)
11 Definition MorphismInTo `{C:Category}(X:C) := { Y:C & Y~~{C}~~>X }.
12 Definition MorphismOutOf `{C:Category}(X:C) := { Y:C & X~~{C}~~>Y }.
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) }.
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) _
25 destruct f. destruct g. destruct H0. destruct H1. simpl in *. setoid_rewrite <- e. setoid_rewrite <- e0. apply associativity.
28 simpl; setoid_rewrite associativity. reflexivity.
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.
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) _
44 destruct f. destruct g. destruct H0. destruct H1. simpl in *. setoid_rewrite <- associativity.
45 setoid_rewrite e. auto.
48 simpl; setoid_rewrite associativity. reflexivity.
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.