Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 26 May 1995 10:21:37 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA050928110; Fri, 26 May 1995 02:48:30 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from emu.pmms.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA050017789; Fri, 26 May 1995 02:43:09 -0600 Received: by emu.pmms.cam.ac.uk (UK-Smail 3.1.25.1/1); Fri, 26 May 95 08:53 BST Message-Id: Date: Fri, 26 May 95 09:42 BST From: Thomas Forster To: Malcolm.Newey@cs.anu.edu.au, info-hol@leopard.cs.byu.edu Subject: Re: Curry and uncurry Ray Toal says: > Of course you do not *need* the type pair at all in Type Theory. > It is not primitive. Probably what you could say is that > pairs do not exist and that f(a,b) is just syntactic sugar > for f a b. Hmmmm so what do you make of functions from N to N * N?