open import 1Lab.Prelude

open import Cat.Base

module Cat.Instances.Shape.Initial where

open Precategory

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 ._=>_.is-natural ()