major revision: separate Subcategory into {Wide,Full}Subcategory

[coq-categories.git] / src / InitialTerminal_ch2_2.v

diff --git a/src/InitialTerminal_ch2_2.v b/src/InitialTerminal_ch2_2.v
index af69c6a..c76208e 100644 (file)
--- a/src/InitialTerminal_ch2_2.v
+++ b/src/InitialTerminal_ch2_2.v
@@ -8,27 +8,42 @@ Require Import Isomorphisms_ch1_5.
 (* Chapter 2.2: Initial and Terminal Objects                                  *)
 (******************************************************************************)
 
-(* Definition 2.7 *)
-Class Initial
-`( C            : Category                         ) :=
-{ zero          : C
+Class InitialObject
+`{ C            : Category                         }
+ ( initial_obj  : C                                ) :=
+{ zero          := initial_obj
 ; bottom        : forall a,  zero ~> a
 ; bottom_unique : forall `(f:zero~>a), f ~~ (bottom a)
 }.
 Notation "? A" := (bottom A)     : category_scope.
 Notation "0"   := zero           : category_scope.
+Coercion zero : InitialObject >-> ob.
+Implicit Arguments InitialObject [[Ob][Hom]].
 
-(* Definition 2.7 *)
-Class Terminal
-`( C          : Category                         ) :=
-{ one         : C
+Class TerminalObject
+`{ C             : Category                       }
+ ( terminal_obj  : C                              ) :=
+{ one         := terminal_obj
 ; drop        : forall a,  a ~> one
 ; drop_unique : forall `(f:a~>one), f ~~ (drop a)
 }.
 Notation "! A" := (drop A)       : category_scope.
 Notation "1"   := one            : category_scope.
+Coercion one : TerminalObject >-> ob.
+Implicit Arguments TerminalObject [[Ob][Hom]].
 
 
-(* Proposition 2.8 *)
-(* FIXME: initial and terminal objects are unique up to iso *)
+(* initial objects are unique up to iso *)
+Lemma initial_unique_up_to_iso `{C:Category}{io1:C}(i1:InitialObject C io1){io2:C}(i2:InitialObject C io2) : io1 ≅ io2.
+  refine {| iso_backward := bottom(InitialObject:=i2) io1 ; iso_forward := bottom(InitialObject:=i1) io2 |}.
+  setoid_rewrite (bottom_unique(InitialObject:=i1)); reflexivity.
+  setoid_rewrite (bottom_unique(InitialObject:=i2)); reflexivity.
+  Qed.
+
+(* terminal objects are unique up to iso *)
+Lemma terminal_unique_up_to_iso `{C:Category}{to1:C}(t1:TerminalObject C to1){to2:C}(t2:TerminalObject C to2) : to1 ≅ to2.
+  refine {| iso_backward := drop(TerminalObject:=t1) to2 ; iso_forward := drop(TerminalObject:=t2) to1 |}.
+  setoid_rewrite (drop_unique(TerminalObject:=t1)); reflexivity.
+  setoid_rewrite (drop_unique(TerminalObject:=t2)); reflexivity.
+  Qed.