Terminal categories

We prove that a category is terminal if its underlying type has a Unique structure and the category has an IsDiscrete instance.

We then use this to provide various examples of terminal categories.

TODO: Show the converse: that terminal categories have a unique object and are discrete.

TODO: Provide an analogous characterization of terminal categories as codiscrete categories with a unique object.

def CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete {T : Type u} [Category.{v, u} T] [Unique T] [IsDiscrete T] : Limits.IsTerminal (of T)

A discrete category with a unique object is terminal.

Equations

• CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete = CategoryTheory.Limits.IsTerminal.ofUniqueHom (fun (X : CategoryTheory.Cat) => (CategoryTheory.Functor.const ↑X).obj default) ⋯

instance CategoryTheory.Cat.instHasTerminal : Limits.HasTerminal Cat

noncomputable def CategoryTheory.Cat.terminalIsoOfUniqueOfIsDiscrete {T : Type u} [Category.{v, u} T] [Unique T] [IsDiscrete T] : ⊤_ Cat ≅ of T

Any T : Cat.{u, u} with a unique object and discrete homs is isomorphic to ⊤_ Cat.{u, u}.

Equations

• CategoryTheory.Cat.terminalIsoOfUniqueOfIsDiscrete = CategoryTheory.Limits.terminalIsoIsTerminal CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete

def CategoryTheory.Cat.isTerminalDiscretePUnit : Limits.IsTerminal (of (Discrete PUnit.{u_1 + 1}))

The discrete category on PUnit is terminal.

Equations

• CategoryTheory.Cat.isTerminalDiscretePUnit = CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete

def CategoryTheory.Cat.isoDiscretePUnitOfIsTerminal {T : Type u} [Category.{u, u} T] (hT : Limits.IsTerminal (of T)) : of T ≅ of (Discrete PUnit.{u + 1})

Any terminal object T : Cat.{u, u} is isomorphic to Cat.of (Discrete PUnit).

Equations

• CategoryTheory.Cat.isoDiscretePUnitOfIsTerminal hT = hT.uniqueUpToIso CategoryTheory.Cat.isTerminalDiscretePUnit