From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a1c:4c9:: with SMTP id 192-v6mr187046wme.8.1527687673157;
        Wed, 30 May 2018 06:41:13 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:adf:dd88:: with SMTP id x8-v6ls2550192wrl.9.gmail; Wed, 30
 May 2018 06:41:12 -0700 (PDT)
X-Received: by 2002:adf:9141:: with SMTP id j59-v6mr256867wrj.3.1527687672503;
        Wed, 30 May 2018 06:41:12 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1527687672; cv=none;
        d=google.com; s=arc-20160816;
        b=DAI6Ke9Fgk5XcWGABUr4BgpfPUv6afu1/OMJCUxLzI7xDBLXOFV+dhoX1TNgGvNGAK
         O9wBBpDCyIZCDRPKZNQq+eNZrTNVQciezpW+9e4tgXToEoyBsYZbcR2UIHm/+WuVpZ+C
         lVg+d8Qsk4R1RVeRi6/bnoT71vcmbQMWMNG3yYdK6ukxkNsw+f2G2rXtpVX7sA6VDQDl
         GWTj5gK+QqfqAHDFnzpAw3r1WAGfYDYMC8S9wrLOu4OW/BWwsmro5PNvUGlbJyFtum+u
         8bgxTzwazEnSSzmFL3ZT+T/c8kB+cWWgqAcns46pFnIOiz2LY5hgPnRuxypxjCRWCuAF
         72aQ==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=user-agent:in-reply-to:content-disposition:mime-version:references
         :message-id:subject:cc:to:from:date:arc-authentication-results;
        bh=tFxYFfD2mHqYDeqw71lMdBl/GZZc3N71nD3mm46haas=;
        b=uhI0xB9885iw3qWENiZoyzNGNc6sD87QGfpxvKPTPoUt1YrOO/RpflQ3ksfWvU62/a
         qdro3UWbh++/sxveyKJCiBs+lhjFQpa372exDgJw24zqVC2TtnGKIR//kY2eKG4gq+bu
         ZD6FD9Q1+cI0R9Lma5hoBOSis2Aj+HIBW55iS0uQtg02eIV+CEsBWE5gnhfI7kQGgcy5
         67VVxUQtlgn59oVeXFgjqmTk+Dqw9b8tu2TwO1PJKkQPhuUnJ/jTxSfLv8NUmVcb7B6w
         WCYxuKgPFE/zHsUsTA7BSyGVUquZT9qqUSWcqeH/zV+ZJddzsRHUTpgiibAQ73p3GqQE
         QjNw==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx503.hrz.tu-darmstadt.de (mail-relay239.hrz.tu-darmstadt.de. [130.83.156.239])
        by gmr-mx.google.com with ESMTPS id x3-v6si269712wrn.0.2018.05.30.06.41.12
        for <homotopyt...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Wed, 30 May 2018 06:41:12 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239;
Authentication-Results: gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21])
	by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id w4UDeKmF022954;
	Wed, 30 May 2018 15:40:25 +0200
	(envelope-from stre...@mathematik.tu-darmstadt.de)
Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209])
	by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id w4UDevi6006116;
	Wed, 30 May 2018 15:40:57 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id ECDD21A0C44; Wed, 30 May 2018 15:40:56 +0200 (CEST)
Date: Wed, 30 May 2018 15:40:56 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
Cc: Michael Shulman <shu...@sandiego.edu>,
        "homotopyt...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Re: Where is the problem with initiality?
Message-ID: <20180530134056.GA4374@mathematik.tu-darmstadt.de>
References: <CAOvivQxmrTLRW8wk7cu+A9zF3LCrXSfqsp6R2UN_sz9tF-5UHQ@mail.gmail.com>
 <CAOvivQyY1k+KE9PztsNq6uhZGuV9D3pOYznnbB4p81s4=iHK0g@mail.gmail.com>
 <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk>
 <CAOvivQw+-fuPg=8gd=cvTsY++iqH4+=B4QRHQcm8vK6FwQSkGg@mail.gmail.com>
 <20180530093331.GA28365@mathematik.tu-darmstadt.de>
 <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk>
 <20180530101041.GA30885@mathematik.tu-darmstadt.de>
 <F4B2CB88-E830-4EB5-B234-09F3E2D29862@exmail.nottingham.ac.uk>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <F4B2CB88-E830-4EB5-B234-09F3E2D29862@exmail.nottingham.ac.uk>
User-Agent: Mutt/1.5.23 (2014-03-12)
X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2018.5.30.115718
X-PMX-RELAY: outgoing

On Wed, May 30, 2018 at 12:08:37PM +0000, Thorsten Altenkirch wrote:
> Names are syntactic sugar. 
> 
> In the intrinsic syntax ine uses a form of typed de Bruijn. To relate them to name carrying syntax is straight forward.

de Bruijn is just one part of the algebraization of syntax

the algebraic language constains much more inclusing an awful lot of
typing information which is usually inferred

Thomas