[Haskell-cafe] Categorical description of systems with dependent types

roconnor at theorem.ca roconnor at theorem.ca
Thu Dec 2 17:18:21 CET 2010

On Thu, 2 Dec 2010, Petr Pudlak wrote:

> Hi,
> recently, I was studying how cartesian closed categories can be used to 
> describe typed functional languages. Types are objects and morphisms are 
> functions from one type to another.
> Since I'm also interested in systems with dependent types, I wonder if there 
> is a categorical description of such systems. The problem (as I see it) is 
> that the codomain of a function depends on a value passed to the function.
> I'd happy if someone could give me some pointers to some papers or other 
> literature.

Voevodsky talks about the category of contexts in 
<http://www.mefeedia.com/watch/31778282>, which I understand is described 
in more detail in "Semantics of type theory : correctness, completeness, 
and independence results" by Thomas Streicher.

Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

More information about the Haskell-Cafe mailing list