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 Class InitialObject
  12 `{ C            : Category                         }
  13  ( initial_obj  : C                                ) :=
  14 { zero          := initial_obj
  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 Coercion zero : InitialObject >-> ob.
  21 Implicit Arguments InitialObject [[Ob][Hom]].
  22
  23 Class TerminalObject
  24 `{ C             : Category                       }
  25  ( terminal_obj  : C                              ) :=
  26 { one         := terminal_obj
  27 ; drop        : forall a,  a ~> one
  28 ; drop_unique : forall `(f:a~>one), f ~~ (drop a)
  29 }.
  30 Notation "! A" := (drop A)       : category_scope.
  31 Notation "1"   := one            : category_scope.
  32 Coercion one : TerminalObject >-> ob.
  33 Implicit Arguments TerminalObject [[Ob][Hom]].
  34
  35
  36 (* initial objects are unique up to iso *)
  37 Lemma initial_unique_up_to_iso `{C:Category}{io1:C}(i1:InitialObject C io1){io2:C}(i2:InitialObject C io2) : io1 ≅ io2.
  38   refine {| iso_backward := bottom(InitialObject:=i2) io1 ; iso_forward := bottom(InitialObject:=i1) io2 |}.
  39   setoid_rewrite (bottom_unique(InitialObject:=i1)); reflexivity.
  40   setoid_rewrite (bottom_unique(InitialObject:=i2)); reflexivity.
  41   Qed.
  42
  43 (* terminal objects are unique up to iso *)
  44 Lemma terminal_unique_up_to_iso `{C:Category}{to1:C}(t1:TerminalObject C to1){to2:C}(t2:TerminalObject C to2) : to1 ≅ to2.
  45   refine {| iso_backward := drop(TerminalObject:=t1) to2 ; iso_forward := drop(TerminalObject:=t2) to1 |}.
  46   setoid_rewrite (drop_unique(TerminalObject:=t1)); reflexivity.
  47   setoid_rewrite (drop_unique(TerminalObject:=t2)); reflexivity.
  48   Qed.
  49