Strict initial object (source code)

= Strict initial object

An <initial object> $0$ is strict when every <morphism> into $0$ is invertible. Adjoining a new strict initial object to a <category> means adding one map from it to every object and no map to it from any old object. Its only endomorphism is the identity.