Limits and colimits indexed by Fin

In this file, we show that 0 : Fin (n + 1) is an initial object and Fin.last n is a terminal object. This allows to compute limits and colimits indexed by Fin (n + 1), see limitOfDiagramInitial and colimitOfDiagramTerminal in the file Limits.Shapes.IsTerminal.

def Fin.isInitialZero (n : ℕ) [NeZero n] : CategoryTheory.Limits.IsInitial 0

0 is an initial object in Fin n when n ≠ 0.

Equations

• Fin.isInitialZero n = CategoryTheory.Limits.isInitialBot

def Fin.isTerminalLast (n : ℕ) : CategoryTheory.Limits.IsTerminal (last n)

Fin.last n is a terminal object in Fin (n + 1).

Equations

• Fin.isTerminalLast n = CategoryTheory.Limits.isTerminalTop