From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a50:c30b:: with SMTP id a11-v6mr890402edb.8.1527675061168;
        Wed, 30 May 2018 03:11:01 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a50:fc19:: with SMTP id i25-v6ls499949edr.0.gmail; Wed, 30
 May 2018 03:11:00 -0700 (PDT)
X-Received: by 2002:a50:8e14:: with SMTP id 20-v6mr886125edw.3.1527675060084;
        Wed, 30 May 2018 03:11:00 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1527675060; cv=none;
        d=google.com; s=arc-20160816;
        b=QZ5yXlgazyzpPOzFLpKZhUbicvRMhb59dTyiPtt5A7qtzTX93ti5aDeeFWOG2ty5SC
         wLW8MTxC0Ugn+u9vB5i1mvifVIFXkHKi3MwMqsQwsj0AB38iRZjGLfyPkv5L2dXcOmLT
         hwQYucmuzXO35VVojInFseqY8LeQ7JgEUnT/zQwSlR1ETIc4PTw3/zYrfygRVnJ52UN9
         1ll1IKCfiYJNGTEVwofNpVi2W+odeXiRUrHsrBcUlGAS5Kocb0D9oXefyOdNDAeoVXmH
         5QjDotC8PJDzhOpsuhde+VEha2V4vnyqU388XtELvyeSHBr0P0BVGqRhDOFWm5dGmrbx
         0Dow==
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=CjiXyh52G7ZZGp+rAnkIo0IfnCWEw8EWxYJCtujh6jc=;
        b=c0wxwTK70QCsjSE3vYMXcdc5nn7B63r/9pfNMa87yi2Cv/avtzTXtJOVSgHpAYnAub
         iRI7sUV6vAkCm2wYGRxQZqe+S1VumztvTFA9PXR4B2k0/eWyv5o8d+2lpXXwHEQKJBC2
         ZrAO6Mf7styGkimT2R2elcXQ2NrWkJI3Bo0vdDCqDXPohibukE2eORg+CGKQnuaOMJhH
         1LDZOm0g3o0tdIaJk4gmblwNlAQnwr57YtKTdf+8A9RRJLhIjmviy1sJBN6PZhu5X4wJ
         k2hR8INBPQL3gFcCm6m0K31t7OtKEFht6MfxtsoqX7IiElq6ltqqFDUrAKv3BSmXDfeX
         Ynng==
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 z2-v6si1225027edq.2.2018.05.30.03.10.59
        for <homotopyt...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Wed, 30 May 2018 03:11:00 -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 w4UAA5hF018661;
	Wed, 30 May 2018 12:10:11 +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 w4UAAfi6003726;
	Wed, 30 May 2018 12:10:41 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 53DCF1A0C44; Wed, 30 May 2018 12:10:41 +0200 (CEST)
Date: Wed, 30 May 2018 12:10:41 +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: <20180530101041.GA30885@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>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <5559377C-94C9-422E-BBF7-A07AFA4B7D04@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.100016
X-PMX-RELAY: outgoing

> On 30/05/2018, 10:33, "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de> wrote:
> 
>     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.
> 
> For the human mind accustomed to the separation of collections and predicates as present in conventional Mathematics.

That we have in TT as well turning a predicate P on A into the type
(Sigma x:A) P(x).

But that's not the issue here. Its rather syntax with variables as
opposed to syntax with combinators.

In topos theory performing arguments within internal language giving
the illusion of elements is much simpler than chasing diagrams. The
former seems closer to how our mind seems to work. But not verything
can be done internally. Mathematics is all internal, it's logic which
can speak also about the external.

Thomas