src/InitialTerminal_ch2_2.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 2.2: Initial and Terminal Objects                                  *)
   9 (******************************************************************************)
  10
  11 (* Definition 2.7 *)
  12 Class Initial
  13 `( C            : Category                         ) :=
  14 { zero          : C
  15 ; bottom        : forall a,  zero ~> a
  16 ; bottom_unique : forall `(f:zero~>a), f ~~ (bottom a)
  17 }.
  18 Notation "? A" := (bottom A)     : category_scope.
  19 Notation "0"   := zero           : category_scope.
  20
  21 (* Definition 2.7 *)
  22 Class Terminal
  23 `( C          : Category                         ) :=
  24 { one         : C
  25 ; drop        : forall a,  a ~> one
  26 ; drop_unique : forall `(f:a~>one), f ~~ (drop a)
  27 }.
  28 Notation "! A" := (drop A)       : category_scope.
  29 Notation "1"   := one            : category_scope.
  30
  31
  32 (* Proposition 2.8 *)
  33 (* FIXME: initial and terminal objects are unique up to iso *)
  34