This page is part of the Initiality Project.
I suspect that the easiest way to prove uniqueness will be to use the initial object lemma: if is an object of a category equipped with a natural transformation from the constant functor at to the identity functor such that the component is the identity morphism, then 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.
TODO
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.