Library InitialTerminalCategory


Require Import Utf8.
Require Export Category Functor.
Require Import DiscreteCategory.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

Initial and terminal objects of the category of categories.


Section InitialTerminal.
  Definition TerminalCategory : @SmallCategory unit :=
    Eval compute in DiscreteCategory unit.
  Definition InitialCategory : (@SmallCategory ) :=
    Eval compute in DiscreteCategory .
End InitialTerminal.

Section InitialTerminalFunctors.
  Context `(C : @Category objC).

  Definition FunctorToTerminal : Functor C TerminalCategory
    := Build_Functor C TerminalCategory (fun _tt) (fun _ _ _eq_refl) (fun _ _ _ _ _eq_refl) (fun _eq_refl).

  Definition FunctorFromTerminal (c : C) : Functor TerminalCategory C
    := Build_Functor TerminalCategory C (fun _c) (fun _ _ _Identity c) (fun _ _ _ _ _eq_sym (@RightIdentity _ _ _ _ _)) (fun _eq_refl).

  Definition FunctorFromInitial : Functor InitialCategory C
    := Build_Functor InitialCategory C (fun xmatch x with end) (fun x _ _match x with end) (fun x _ _ _ _match x with end) (fun xmatch x with end).
End InitialTerminalFunctors.

Coercion FunctorFromTerminal : Object >-> Functor.