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, <rocon...@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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe