From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.223.160.114 with SMTP id l47mr377631wrl.29.1507974766445;
        Sat, 14 Oct 2017 02:52:46 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.191.29 with SMTP id p29ls593105wmf.8.canary-gmail; Sat, 14
 Oct 2017 02:52:45 -0700 (PDT)
X-Received: by 10.28.138.130 with SMTP id m124mr421186wmd.27.1507974765601;
        Sat, 14 Oct 2017 02:52:45 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1507974765; cv=none;
        d=google.com; s=arc-20160816;
        b=aoVkC3vGPzf3zC7Nhvck41jvPvfXCi6jhoTr7qmTFP3iaJxR1fBYRcy4MzlIilbmyy
         xQtc9pthurJoSUCGmn9KLha3l8mrmC1C5xotZ3QsJmIpbT/S+Kcr2xDSfn48hcdC1bUC
         UsvHxlYKzkGywqtoizdtwiXKyVbcNztC5JMyyhqwmINXRH5RCuRUGCfzOfQV1to2paaB
         kT9WRNbQ+s7ZbsHDelW05Fun9yWJshfNwbg1FZr8r2AupDYxG7CJM9kj+AveLdHBdseA
         HCHz3JSF4BucYPai7dATPFjxfz07mLfnN7mTd1j0/qnT2Rz19HzWSNTgRZ4NpNr5vwm5
         w/nw==
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=Ju2Ir+as2ruoF/Sh6OeCYgUJ5RCioJ7+AasNskpLTNQ=;
        b=UaepVTtfQuS1wC9Ytlht7v7NdjxpAyTqyZUCfU4aWCQSVDeTUvHQM0QirftPcIqmxS
         OCer7aOfWEipESnxlzqUFXCUgIB6cYgLVzykq+Cgu/HFPmJpxExF8RedsEBUrw68OYQt
         AJCjXwvz7Y7fDbZbgrwE+aAGi3e2wZxbYwcOGnOTaaQmQ/DY9dMeL2lef4kr+DNGgU4l
         A2/bXJle1wRcu6/pYiXopMKupM0/c0xWLQi0yR23vzyxRXjqYuhqHGlwQak2ZmAEMMEX
         3v2qHCviqgxFLZFZEwiVInrI3aljjaP8f2Fjxei+J4EDz9dVjyI602GP9M3YtP+BkNnK
         Lrlg==
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.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx500.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.156.225])
        by gmr-mx.google.com with ESMTPS id b8si96751wrf.5.2017.10.14.02.52.45
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Sat, 14 Oct 2017 02:52:45 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) client-ip=130.83.156.225;
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.225 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 lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v9E9nRKH013747;
	Sat, 14 Oct 2017 11:49:27 +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 v9E9qiRF030925;
	Sat, 14 Oct 2017 11:52:44 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 0E9631A0D1C; Sat, 14 Oct 2017 11:52:44 +0200 (CEST)
Date: Sat, 14 Oct 2017 11:52:43 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Andrej Bauer <andrej...@andrej.com>
Cc: Homotopy Type Theory <homotopyt...@googlegroups.com>,
        Univalent Mathematics <univalent-...@googlegroups.com>
Subject: Re: [HoTT] A small observation on cumulativity and the failure of
 initiality
Message-ID: <20171014095243.GA29903@mathematik.tu-darmstadt.de>
References: <F2106ADB-D78F-4228-B0A9-DBC6EC69E96A@princeton.edu>
 <CAAkwb-kaWf0=SROtXVnHvN5Xb9RJOoQYjXu6i5tonzq0J3o4TQ@mail.gmail.com>
 <20171013081056.GB18718@mathematik.tu-darmstadt.de>
 <D6077B1B.A2237%psztxa@exmail.nottingham.ac.uk>
 <CAB0nkh1dApftkpR+KWJS445wxcab2zqt6o1FBgybjCrc-U0neA@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <CAB0nkh1dApftkpR+KWJS445wxcab2zqt6o1FBgybjCrc-U0neA@mail.gmail.com>
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: 2017.10.14.94516
X-PMX-RELAY: outgoing

Andrej,

you are right in the sense that the free model of a certain type
theory T is not trivially isomorphic the syntax modulo. The late
Voevodsky suggested this to be an important problem and Peter
Lumsdaine has worked on it for some time.
It feels a bit like a non-mathematical problem in the sense of being
more organizational or CS like. But maybe one should think about ways
to introduce variables in a systematic way for making categorical
combinator based syntax more palatable. There is more hope this way
get something than strating from raw syntax and how to tame it
semantically.

Thomas