Library HoTT.Categories.InitialTerminalCategory.Core

Initial and terminal category definitions

Require Import HoTT.Basics HoTT.Types.
Require Import Category.Core.
Require Import NatCategory.

Set Implicit Arguments.
Generalizable All Variables.
Local Unset Primitive Projections. (* suppress a warning about IsTerminalCategory *)

Notation initial_category := (nat_category 0) (only parsing).
Notation terminal_category := (nat_category 1) (only parsing).

Terminal categories

A precategory is terminal if its objects and morphisms are contractible types.
Class IsTerminalCategory (C : PreCategory)
      `{Contr (object C)}
      `{∀ s d, Contr (morphism C s d)}
  : Type0 := {}.

Initial categories

An initial precategory is one whose objects have the recursion principle of the empty type
Class IsInitialCategory (C : PreCategory)
  := initial_category_ind : ∀ P : Type, C → P.

Instance trunc_initial_category `{IsInitialCategory C}
: IsHProp C
  := istrunc_S _ (fun x y ⇒ initial_category_ind _ x).
Instance trunc_initial_category_mor `{IsInitialCategory C} x y
: Contr (morphism C x y)
  := initial_category_ind _ x.

Default initial (0) and terminal (1) precategories.

Instance is_initial_category_0 : IsInitialCategory 0 := (fun T ⇒ @Empty_ind (fun _ ⇒ T)).
Instance: IsTerminalCategory 1 | 0 := {}.
Instance: Contr (object 1) | 0 := _.
Instance : `{Contr (morphism 1 x y)} | 0 := fun x y ⇒ _.
Instance default_terminal C {H H1} : @IsTerminalCategory C H H1 | 10 := {}.

Arguments initial_category_ind / .
Arguments is_initial_category_0 / .