module Cat.Instances.Shape.Initial where

The initial category is the category with no objects.

⊥Cat : Precategory lzero lzero
⊥Cat .Ob = 
⊥Cat .Hom _ _ = 

This category is notable for the existence of a unique functor from it to any other category.

module _ {o h} {A : Precategory o h} where
  private module A = Precategory A
  open Functor

  ¡F : Functor ⊥Cat A
  ¡F .F₀ ()

  ¡F-unique :  (F G : Functor ⊥Cat A)  F  G
  ¡F-unique F G i .F₀ ()

  ¡nt :  {F G : Functor ⊥Cat A}  F => G
  ¡nt ._=>_.η ()
  ¡nt ._=> ()