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 (******************************************************************************)
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.
25 ; drop : forall a, a ~> one
26 ; drop_unique : forall `(f:a~>one), f ~~ (drop a)
28 Notation "! A" := (drop A) : category_scope.
29 Notation "1" := one : category_scope.
33 (* FIXME: initial and terminal objects are unique up to iso *)