From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.28.209.72 with SMTP id i69mr432417wmg.10.1513701102513;
        Tue, 19 Dec 2017 08:31:42 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.223.161.27 with SMTP id o27ls5362686wro.2.gmail; Tue, 19 Dec
 2017 08:31:41 -0800 (PST)
X-Received: by 10.28.184.200 with SMTP id i191mr387600wmf.7.1513701101478;
        Tue, 19 Dec 2017 08:31:41 -0800 (PST)
ARC-Seal: i=1; a=rsa-sha256; t=1513701101; cv=none;
        d=google.com; s=arc-20160816;
        b=HIxpupVfqYlvJO0fofvtHuCEAPdQ7MmHhJe7IThpbPe9BQ/IiyVkVk/IpJLglX+3Vd
         vSbZf46ZWz1yNRx/zcV75ujtUrAwceFnVSJn99uDO+GKeZIxb10+RcluOl4T4M36nvOJ
         QxGNlSyIwSwvj4nk1cqNRG8YkNQEeZzCFm/BOTBOcnNAblGk3BN7Zl8bV0dCpOMBVojb
         OQ1hubZKVtjiCb5jTbiKXuaEwYEQHKXvWKFG7ZJMfFfEDPC+BQRkkc8dYhQGGL+KlXxp
         rGlMrQnQ8yVywaKUiK96f9BIQHyvSTfptRSWskQ/Nt81sPySz9A2kIy6pz8bb/53b5UO
         PApA==
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=sdFUtdMIL9tgYJJOhk4LGpR1vBFmVtf1i4b6CpRF4NI=;
        b=gfrDb4nZx9C0H/0NTuCW/cuC/0+QuxmhCQCpupgLerxHKpfMeeNYIzaPAuTY1cU9Vz
         fB8MJhptyoeuPpE0/Z5PYc/T+iXGHOeRNc6FwNJNE0UM2GqkDarrpS6x3rlx3z2Vd2ju
         sf+q4LE3nQTtCKm2TP+UUCV0Vc3AiBNFRnLaYlnsL5Hqu86zYj1AQRgm1bmwug+Gdbx6
         MwpL7P+Nr1fsWiSvu3zFE08goG1gC2A1QiPufGELMvqpXrIf9luzNye2xEf4ay3Zwhmj
         w/BcIv4eY+AQc8LkcfQ/2/rqYMfbRSq6YsMA5nS7cR7RpIptsqsxcBKUGy5TKD0usOxc
         9dhw==
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 h76si186707wmd.1.2017.12.19.08.31.41
        for <homotopyt...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Tue, 19 Dec 2017 08:31:41 -0800 (PST)
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 vBJGQdwb013930;
	Tue, 19 Dec 2017 17:26:39 +0100
	(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 vBJGVdRF026583;
	Tue, 19 Dec 2017 17:31:39 +0100
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id A85C41A0D60; Tue, 19 Dec 2017 17:31:39 +0100 (CET)
Date: Tue, 19 Dec 2017 17:31:39 +0100
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
Cc: Andrej Bauer <andrej...@andrej.com>,
        Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof
 irrelevance consistent?
Message-ID: <20171219163139.GB13875@mathematik.tu-darmstadt.de>
References: <20171215170011.GA22027@mathematik.tu-darmstadt.de>
 <D65BDF23.A4EFB%psztxa@exmail.nottingham.ac.uk>
 <20171217102151.GA16619@mathematik.tu-darmstadt.de>
 <D65C0347.A4F0B%psztxa@exmail.nottingham.ac.uk>
 <20171218115228.GB29410@mathematik.tu-darmstadt.de>
 <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk>
 <CAB0nkh1s1Z_Fdn8_btnb+0auM+OfiYTuAmqaGdmAkEKfkhnOuQ@mail.gmail.com>
 <A336FB3E-8247-4240-A034-3119B1C516FB@exmail.nottingham.ac.uk>
 <20171219153118.GA9218@mathematik.tu-darmstadt.de>
 <D55DEF85-61F6-480E-B627-B59CE5DBD481@exmail.nottingham.ac.uk>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <D55DEF85-61F6-480E-B627-B59CE5DBD481@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: 2017.12.19.162416
X-PMX-RELAY: outgoing

> Ah, you suffer from using set theory as a meta language. (
> 
> There are lots if univalent categories. In HoTT.

That clears it up!

Thomas

PS  I am not fixed to set theory. Could as well be a suffiently strong
extensional type theory. But, of course, set theory is fine for me as
a metalanguage.