nLab Initiality Project - Uniqueness

Initiality Project - Uniqueness

This page is part of the Initiality Project.

Overview

I suspect that the easiest way to prove uniqueness will be to use the initial object lemma: if $I$ is an object of a category $D$ equipped with a natural transformation $\iota$ from the constant functor $\Delta I$ at $I$ to the identity functor $Id_D$ such that the component $\iota_I : I\to I$ is the identity morphism, then $I$ is an initial object.

This means we have two things to prove: that the interpretation functor?s are natural, and that the interpretation functor into the term model itself is the identity. I believe that both should be provable by induction over raw syntax with reference only to the partial interpretation functions, since we have separately proved that these partial functions happen to be total.

Naturality

TODO

The tautological interpretation

TODO

category: Initiality Project