From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a1c:8702:: with SMTP id j2-v6mr130669wmd.1.1527672813860;
        Wed, 30 May 2018 02:33:33 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:adf:dd51:: with SMTP id u17-v6ls3452660wrm.12.gmail; Wed, 30
 May 2018 02:33:33 -0700 (PDT)
X-Received: by 2002:adf:b69f:: with SMTP id j31-v6mr163801wre.29.1527672813082;
        Wed, 30 May 2018 02:33:33 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1527672813; cv=none;
        d=google.com; s=arc-20160816;
        b=y2D0G1YjW6dvL28fc7QHxWnqtTtIpDo7tiWC0JVmoacpV08YjiAbo+jHNhlkCJPbzD
         HmB8pkZ8tPj9YyMYWiazp88jSfmUlgznA1G0FUvYw413HHPP+tDsIl9t1T7MwsiGhTyM
         kuFoKjAzEdDlf03uxDliqG0KmuVwnuvF2fxDS1A/QGuuw333hD84XTu7RzEJg5nJGyVL
         cf+o9kMQW35ajNc6u+VsnxNaB42IBX9HcyesoZcu1oCicaKXsYWJo78jblv+rc87Mtgy
         KaSX1k6nATaQHJYYFXfACmsdGxgZGXSDD//4AnyF7kNqjJvqv4ajAdZaBlLWmA0jiXuU
         dgvg==
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=ctvYox9NzK8ON4r6WkIDVBzVgveL8GmVDxP03AiLxv8=;
        b=mYK1IYTHzC+2N/O77/xvsDiksLxt4pRcMhbGEj2HAqrNpj8ZB0WeHXU5L/lbkvVTL5
         9aI0QSRIPQCWuznvGxN04ZjC8ZW4OKyj3Bp0Tvq+bB31VjsScZGgn2pylME/IoFwDB5k
         op0BjEs0ULabfnqfqsyosr117I4/RL4EquDsF1cGs4FvLONRoJ1GtPofHAJB+aIribC6
         v/bgvbSeBy73kK1pOIdvyHpj4bnWhcBqp5ET9vcn8j4Stq7CWJXwdp3JLrt5ef7ChSJU
         1gDhu3RtdPml1yrRtFtyXIy33uexxnQn6Ngbw8aA/FkQsQx8wpFskoVD5TovF+WS7GYb
         GB5g==
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-v6si244638wrn.0.2018.05.30.02.33.32
        for <homotopyt...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Wed, 30 May 2018 02:33:33 -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 w4U9Wton012149;
	Wed, 30 May 2018 11:32:55 +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 w4U9XVi6003182;
	Wed, 30 May 2018 11:33:31 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 537151A0C44; Wed, 30 May 2018 11:33:31 +0200 (CEST)
Date: Wed, 30 May 2018 11:33:31 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Michael Shulman <shu...@sandiego.edu>
Cc: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>,
        "homotopyt...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Re: Where is the problem with initiality?
Message-ID: <20180530093331.GA28365@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>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <CAOvivQw+-fuPg=8gd=cvTsY++iqH4+=B4QRHQcm8vK6FwQSkGg@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: 2018.5.30.92416
X-PMX-RELAY: outgoing

In my eyes the so called initiality problem is not a problem of
semantics of type theory. Models of type theory are essentailly
algebraic objects and thus as observed by Vladimir do admit an initial
one.

Syntax based on categorical combinatorsis fine in principle and useful
for implementaion.

That categorical syntax and ordinary syntax are isomorphic is just a
purely syntactic result allowing one to replace correct algebraic
syntax by one more accessible for the human mind. But it is important
to show that this replacement is faithful w.r.t. the mathematically
correct one.

Thomas