The Coq mailing list

[Eduardo Ochs <eduardoochs AT gmail.com>]

Hi list,

I am preparing a presentation about the Calculus of Constructions for (basic) Category Theory students and I noticed that in most CompSci texts the dependent products, that generate spaces of functions, have a much higher status than the dependent sums, that are usually mentioned just in passing... I come from a CT background, and I remember that in texts about the categorical semantics of type systems (e.g., Bart Jacobs's book) dependent products and dependent sums start with equal status, then at some point - usually as an exercise; but I am recalling this from memory and I don't have the book at hand now, so I may be wrong - it is shown that under certain conditions the existence of dependent products _imply_ the existence of dependent sums...

Can anyone recommend me a place where all this is discussed? I am preparing an introduction, so I'm focused on finding a good dydactical path... for me the most natural way to present the material is:

  1) the simply-typed lambda-calculus,

  2) dependent types and polymorphism,

  3) Pure Type Systems,

  4) the Barendregt Cube,

  5) dependent sums (and PTSs with them),

  6) proofs-as-types,

  7) inductive types,

  8) CoC and CiC,

  9) dependent sums can be defined from the rest...

But no one seems to take that path.

  Thanks in advance,

    Eduardo Ochs 

    http://angg.twu.net/math-b.html