From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a2e:9e4c:: with SMTP id g12-v6mr798530ljk.37.1527919306841;
        Fri, 01 Jun 2018 23:01:46 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a19:cf0e:: with SMTP id f14-v6ls4600729lfg.5.gmail; Fri, 01
 Jun 2018 23:01:45 -0700 (PDT)
X-Received: by 2002:a19:9382:: with SMTP id w2-v6mr77256lfk.28.1527919305976;
        Fri, 01 Jun 2018 23:01:45 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1527919305; cv=none;
        d=google.com; s=arc-20160816;
        b=VGI/ZvJC9u+DvglQ3/EWu8qcHwHNmiEGVPnC+MQCeAz/h9JpLxuEVkFOY33EjrwlDh
         U04hK+BwgyRuezFNHFeIiu2SbxBPKykQ0bVvYIbgqcOadMy9aRodNjChe5KF8uvKZGSA
         SE5YrDMhl4OrXDZClyXCKj5ejIVpTT/Kvk297ERprkGeeOfko9L1WGWUvYrC9o+NRr20
         4teVd+Dn5JeTnQqAbNwM4eyQFOtRaMcjLLnHXXewsdLf+cdXr10TKUFfq9mJM2bVdNA1
         3ws0BOlTvWLGLvTst+0kGnJR0rsNrC6IeO6CyN53VFAXyBbb2p48G77gdWn21xDxGsxZ
         btvA==
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=jmya/cU8Dg0ty7/JG/qvKKhqt/LblrgmbEw2x+O8mgg=;
        b=py5H+t20nSFwzciYyNnBv9nT0xF2EtSdCj6WcE1IgAeLpfbZEAhIJVs3D09yn00RZr
         70EtSkCiuy97WwZb6oCrt8SDePXZYtg6TF6d/aToHXw2NdY0zEiY7pNvpbAecr3FKGRB
         SysCEYu7U/ewrG659wwfM1rxlg9GtmCrlMBkwhjJTx6NB2LXUDFTc6S0G9PlumbgEnxq
         xIouYsYMoVXApiUdZh5zVuI2koDCJneuJXtnpVuO+UqQSDP/wtWCe5D3kur7y+ksmYeQ
         lZ2fSze5JnOdWH/hwXnqiOXWFtbvpb6DeOa1fx6gIhUlD1vLFu772/hUZTM7lq2WS0wD
         unjw==
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 n12-v6si861037lja.4.2018.06.01.23.01.45
        for <HomotopyT...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Fri, 01 Jun 2018 23:01: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 w5260lVD009172;
	Sat, 2 Jun 2018 08:00:47 +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 w5261hi6009047;
	Sat, 2 Jun 2018 08:01:43 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 873B71A0BBF; Sat,  2 Jun 2018 08:01:43 +0200 (CEST)
Date: Sat, 2 Jun 2018 08:01:43 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Ambrus Kaposi <kaposi...@gmail.com>
Cc: atm...@gmail.com, HomotopyT...@googlegroups.com
Subject: Re: [HoTT] Re: Where is the problem with initiality?
Message-ID: <20180602060143.GC7875@mathematik.tu-darmstadt.de>
References: <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com>
 <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>
 <864df164-59e9-4609-8e81-7c334be11e98@googlegroups.com>
 <CACSS4j=rgE5UduE5DMDw3YB5fGXmoW-FJRjyndZSLGpPpYxfBw@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <CACSS4j=rgE5UduE5DMDw3YB5fGXmoW-FJRjyndZSLGpPpYxfBw@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.6.2.55416
X-PMX-RELAY: outgoing

People introduced intensional type theory for having syntax decidable
because that's necessary for convenient implementation.

But any theory appears quotient of N by some r.e. equivalence relation
on N. And isn't the respective quotient always a set?

Thomas