addendum to models of CIC

[Thorsten Altenkirch]

Hi Thomas,

good to hear form you.

Thomas Streicher writes:

 > To my opinion the problem rather is to *fix* a syntactic notion of
 > inductive type (which always will be incomplete) rather than to
 > provide it with a semantics in assemblies.

This is only a problem in intensional Type Theory, in extensional Type
Theory W-types are sufficient. This has been observed by Peter Dybjer
some time ago even though the paper got only published in TCS in 1997.
Recently we (Michael Abbott,Neil Ghani and myselves) have shown that
this also extends to nested datatypes (see
http://www.cs.nott.ac.uk/~txa/publ/wtypes-draft.pdf). Nested types
lead to a little technical problem, because you have to construct an
isomorphism on families - see the paper for details.

 > There is a general non-syntactic notion of inductive type as given by 
 > realizable endo-functors on PER(AA) that preserve coercion maps (those
 > realizable by identity). These induce monotone endomaps on the complete
 > poset (PER(AA),\subseteq) which by Knaster-Tarski do have a fixpoint. There
 > is a general argument showing that these guys coincide with the initial 
 > algebras of the functors (I have a little note on that which I can provide on
 > request). However, alas, from this general treatment it doesn't follow that 
 > these fixpoints are initial in the category of assemblies though in all 
 > interesting cases they are!

I would suggest to use container functors instead - see
http://www.cs.nott.ac.uk/~txa/publ/fossacs03.pdf or Michael Abbott's
http://www.cs.le.ac.uk/~ma139/ very recent PhD thesis (he just passed
his Viva last Friday) The fossacs paper is a bit out of date, I
wouldn't use LFPness anymore.

They also have the advantage that you don't need Knaster-Tarski or any
magic tricks like this... :-) 

Thorsten