The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi Eduardo,

 

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...

 

In most implementations of Type Theory (eg Coq) Sigma-types are built into the structure of inductive definitions. That is you can define Sigma-type as an inductive type but usually people prefer to define specific user defined types instead of explicitly referring to Sigma-types.

 

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.

 

I think PTS are a bit out of date, they emphasize impredicative theories which are hardly practical relevant and which are doubtful from a philosophical point of view (because in my view there is no good justification for impredicative quantification).

 

One reference is the HoTT book, in particular the first chapters.

https://homotopytypetheory.org/book/

I also just finished a book chapter which provides an overview of basic type theory and HoTT based on some courses I have given recently:

http://www.cs.nott.ac.uk/~psztxa/publ/fomus19.pdf

Maybe this could be useful.

 

Cheers,

Thorsten

 

 

 

  Thanks in advance,

    Eduardo Ochs 

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

 

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.