From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a50:e619:: with SMTP id y25-v6mr4502914edm.0.1527916412287;
        Fri, 01 Jun 2018 22:13:32 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a50:fd17:: with SMTP id i23-v6ls3268127eds.6.gmail; Fri, 01
 Jun 2018 22:13:31 -0700 (PDT)
X-Received: by 2002:a50:c30b:: with SMTP id a11-v6mr4494369edb.8.1527916411332;
        Fri, 01 Jun 2018 22:13:31 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1527916411; cv=none;
        d=google.com; s=arc-20160816;
        b=CF3DaFTYJKvi6Z1YypyhmewzNJ1QhvLK5a2+kTU77FXjDDA1L//6xVFmv5JpRsbKq7
         iyvjQNN4ZcmkFNkNjSuItCYRjKK3WaZrljLvoMazJxkYTpgHnHv1fqVy9nWtXPOJKdJ9
         HBMJCYLTxWgVodel3LsLabN5JV86MqJcoRl83iSNMJSwVcLcPKWO8Uvc7CvzZ1MvCZUv
         yl1AGXI2ilIUZoqTWwXKrLSNLFAa/8qcK9Q4hY7FogCjbK9aS6RI8mdc7hcAll9w5hCp
         oo3lQrvSSSM3D/O5LXkRx7m7j6y7o8trZ0US+c3t0SogIj7MpCfIWTAxC/YbdReN+iBp
         Vn/A==
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=mw2KzRC8XK53rO8NDKZeeBLFLqaFX8ibwCIWBg1C9Mw=;
        b=iU5dtbYWQ5h3042b0Bj/LJrgLK/qOklZlStl+K7M1c1IoFZOr8I3kVzVQ08SX78mn8
         q264UW+rPDn76YoZVlqc9ZcEvv3yqAFR1H2FLzzaiKUB2GVVE12o3kmhjGCKt5H0Zhzh
         5KSRnNVvwSSICtMfB5VBBRazA1A0O4PS9Guo6dFqwpvrNvAJ0SONCRDEC47aJ7L4uywj
         EQ0kOuyI7LOGSDa7H50etTL6hh+5hRTFNkYo0wIlSYaAZxz+yciE28449zZRKbctNV0Q
         +9RTWy1HRN5ZVF15zl5VpxOUcFO0G/V9WwmDgOKsFYIQbVEUQOzx7vKzUhuuhnrGlZY8
         9UJg==
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 k6-v6si147735edn.1.2018.06.01.22.13.31
        for <HomotopyT...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Fri, 01 Jun 2018 22:13:31 -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 w525CWSE019867;
	Sat, 2 Jun 2018 07:12:33 +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 w525DSi6008753;
	Sat, 2 Jun 2018 07:13:28 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id B99771A0B6D; Sat,  2 Jun 2018 07:13:28 +0200 (CEST)
Date: Sat, 2 Jun 2018 07:13:28 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: =?iso-8859-1?Q?Mart=EDn_H=F6tzel_Escard=F3?= <escardo...@gmail.com>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Re: Where is the problem with initiality?
Message-ID: <20180602051328.GA7875@mathematik.tu-darmstadt.de>
References: <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk>
 <CAOvivQzSuvhvvhLs0jR2ADTPUR9cKG2NucADJqe=Oer_EB0aaQ@mail.gmail.com>
 <D040F1EA-B812-4703-87CD-840E80DBE5CA@exmail.nottingham.ac.uk>
 <CAOvivQzU1M1gh63RxegZWuzw2LT2b-vsUuSEiB49LAOgJouW6Q@mail.gmail.com>
 <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com>
 <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com>
 <CAGYJgtaFm3OTCWBbeyZrrpVdqYH7GbFbyTT7O9t0gEhSfW5fpg@mail.gmail.com>
 <1efa5fe9-cdc9-4714-ae2a-953ac59cfdf4@googlegroups.com>
 <CAA3CDBagp=z5f-h3gBamc-dV7eUSb07s7eZUwf0qau-efNEZXg@mail.gmail.com>
 <dd79e236-a55d-4f14-b320-41966563bc14@googlegroups.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <dd79e236-a55d-4f14-b320-41966563bc14@googlegroups.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.6.2.50616
X-PMX-RELAY: outgoing

> > I like this question. If the syntax is supposed to be the initial model, 
> >> then it can't be a set.
> >
> >
> > Why? 

It's a decidable prediacte on N and thus a set.

Thomas