nLab Initiality Project - Uniqueness

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 II is an object of a category DD equipped with a natural transformation ι\iota from the constant functor ΔI\Delta I at II to the identity functor Id DId_D such that the component ι I:II\iota_I : I\to I is the identity morphism, then II 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

Last revised on October 28, 2018 at 19:42:45. See the history of this page for a list of all contributions to it.