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

[roconnor at theorem.ca]

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