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

[Iavor Diatchki]

Hi,
Bart Jacobs's book "Categorical Logic and Type Theory" has a
categorical description of a system with dependent types (among
others).  The book is fairly advanced but it has lots of details about
the constructions.
Hope this helps,
-Iavor

On Thu, Dec 2, 2010 at 8:18 AM,  <roconnor at theorem.ca> wrote:
> 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.''
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>