Given a presheaf on a CwF , let , so that is the presheaf consisting of pairs of a type and a type in a context extended by and is the presheaf of pairs of a type and a term in a context extended by .
Let be a CwF. A -type structure on consists of :
exhibiting the following square as a pullback-square
Last revised on November 12, 2018 at 21:53:46. See the history of this page for a list of all contributions to it.