From palmgren@math.uu.se Wed Aug 18 14:47:33 2010 Date: Wed, 18 Aug 2010 14:45:27 +0200 (CEST) From: Erik Palmgren To: logik@math.su.se Cc: Peter Dybjer , Johan Glimming Subject: [logsem] Logikseminariet Stockholm-Uppsala LOGIKSEMINARIET STOCKHOLM-UPPSALA Onsdagen den 25 augusti ges två seminarier i Uppsala: Peter Dybjer (Chalmers) The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theory with Pi, Sigma, and Extensional Identity Types kl 10.30 - 12.15 i sal 2145 (MIC, Polacksbacken, hus 2) Abstract: In his paper Locally cartesian closed categories (1984) and type theory Robert Seely presented a proof that the category LCC of locally cartesian closed categories and the category ML of syntactically presented Martin-Löf type theories (with Pi, Sigma, and extensional identity types) are equivalent. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks in categories. In his paper "Substitution up to isomorphism" Curien (1993) shows that Seely's problem is essentially a coherence problem and proposed how to solve this problem using cut-elimination. An alternative interpretation was then proposed by Hofmann (1994) based on a method due to Benabou. However, neither Curien nor Hofmann showed that their respective interpretations lead to an equivalence between LCC and ML. In this paper we show that Hofmann's interpretation functor gives rise to a biequivalence of 2-categories, and claim that this is the appropriate formulation of Seely's theorem. We replace ML with a categorical analogue CWFLCC of categories with families (with extensional identity types, and Sigma and Pi-types) which are democratic in the sense that each context is represented by a closed type. Most of the difficulty of this proof already appears when relating categories with finite limits (without assuming local cartesian closure) and categories with families without Pi-types. We therefore present this biequivalence (of the 2-categories FL and CWFFL) separately. (Joint work with Pierre Clairambault, PPS, Paris 7) Johan Glimming (Uppsala) Towards Parametric Direcursion kl 14.00-15.45 i rum Å11167 (Ångströmlaboratoriet, hus 1, plan 1, längst söderut) Abstract: Denotational  semantics  of   programming  languages  often  involve recursive function spaces in the domain equation, and for such Freyd proposed  a  recursion  scheme,  called  direcursion,  which  allows definition and proofs, as studied also in the work of Pitts. We will in  this paper  generalise this  mixed-variant recursion  scheme and show that it can be parameterised by an adjunction equipped with two natural  transformations   that  distribute  the  functors   of  the adjunction  in  a  certain   sense  over  the  domain  constructors, generalising   strength  for   endofunctors  to   the  mixed-variant situation.  This gives  also a  generalisation of  enrichment of  an endofunctor  to the  situation  of mixed-variant  functors. The  new recursion scheme, called parametric  direcursion, solves the problem of maintaining  additional arguments while computing  with recursive types.  Applications  are  anticipated   in  the  area  of object-based programming  languages and  normalisation-by-evaluation for  untyped lambda calculus (work in progress). [ Part 2: "Attached Text" ] _______________________________________________ logik@math.su.se mailing list. To unsubscribe or change your subscription options: https://www2.math.su.se/mailman/options/logik?UserOptions=3Dedit Seminar homepage: http://www.math.su.se/~jesper/seminarier/