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 2.2: Initial and Terminal Objects *)
9 (******************************************************************************)
13 ( initial_obj : C ) :=
15 ; bottom : forall a, zero ~> a
16 ; bottom_unique : forall `(f:zero~>a), f ~~ (bottom a)
18 Notation "? A" := (bottom A) : category_scope.
19 Notation "0" := zero : category_scope.
20 Coercion zero : InitialObject >-> ob.
21 Implicit Arguments InitialObject [[Ob][Hom]].
25 ( terminal_obj : C ) :=
27 ; drop : forall a, a ~> one
28 ; drop_unique : forall `(f:a~>one), f ~~ (drop a)
30 Notation "! A" := (drop A) : category_scope.
31 Notation "1" := one : category_scope.
32 Coercion one : TerminalObject >-> ob.
33 Implicit Arguments TerminalObject [[Ob][Hom]].
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.
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.