From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.46.22.20 with SMTP id w20mr271938ljd.38.1513697488124;
        Tue, 19 Dec 2017 07:31:28 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.46.66.3 with SMTP id p3ls2418495lja.11.gmail; Tue, 19 Dec 2017
 07:31:26 -0800 (PST)
X-Received: by 10.25.221.202 with SMTP id w71mr240780lfi.4.1513697486475;
        Tue, 19 Dec 2017 07:31:26 -0800 (PST)
ARC-Seal: i=1; a=rsa-sha256; t=1513697486; cv=none;
        d=google.com; s=arc-20160816;
        b=imTPqj0u1Cl86oZyJYiTbZazhFxTB3U6CeQ6vSW9U7isMMKtqRCyj3Ym+L7gOFatg2
         1cXaZKjpLTDrggAehCCUqtv/03AY+6cGDBJR2KR09mXbVmQ0LKw4LTWCMe1HZtkIYnge
         lLMfhxBYpQ+W/FqnWniwInh+y6bkakHfUCaE3F1plPBngKKl17asfKbXel3O8saQaXTG
         2V3pZjUauUR/y4QYKWF26OaAYKMzijt+ViczmB6i39nxfm6bJm3Bd0NBugMrwUwtZ890
         JnFvveYTE0hIjzv8e04/YOMCorOUeII8A4oR1n+XtLhHUbzI8HYciQc33XgGD+hXzdd2
         Lp2g==
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=totCweq2Jyh88I0cARdhvonCTWi9mdiE055vQc59biw=;
        b=uzIWD7DdUaB0pYZrJjZWo15AiUPwq7+e4NVRBjalGgHsBWrNsOrSzZQhF2h2j/zcPl
         o0XTB+fuJFKFDSqzB0rSRgXKsyH6Lc7KQj29WxqyknpMLOWjz0wR71x5+QheYLn6sAaG
         n65feYuvuRJYZaHsoa1DeNzWfcSpOLHgGY76/Z0t4RfRQh/yAlImspo+v1vEtEH65ER1
         3YhCEvasOsXiQv1UaBwAZekidpj4s+TgBEEcqNcIYpffqTVbYCJaBG9MBP0Yrr4i2DJd
         B4wFL8liLa33SIl8JzZPO1ITkS6ZXvhOU6gtVdYFgxuP61PPtOYleNUGNr2TqW5zybVK
         1DkQ==
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-relay15.hrz.tu-darmstadt.de. [130.83.156.239])
        by gmr-mx.google.com with ESMTPS id c72si583915lfh.5.2017.12.19.07.31.26
        for <homotopyt...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Tue, 19 Dec 2017 07:31:26 -0800 (PST)
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 vBJFVJUN001838;
	Tue, 19 Dec 2017 16:31:21 +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 vBJFVJRF025768;
	Tue, 19 Dec 2017 16:31:19 +0100
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 055D01A0D60; Tue, 19 Dec 2017 16:31:18 +0100 (CET)
Date: Tue, 19 Dec 2017 16:31:18 +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: <20171219153118.GA9218@mathematik.tu-darmstadt.de>
References: <20171212120233.GA32661@mathematik.tu-darmstadt.de>
 <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk>
 <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>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <A336FB3E-8247-4240-A034-3119B1C516FB@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.152415
X-PMX-RELAY: outgoing

>     Furthermore, there can be class-many subobjects of 1 in a topos, for
>     instance in sets there are class-many singletons. Of course, a whole
>     lot of them will be isomorphic and very many "correspond to" the
>     element ??? : ??. But at least on this mailing list we're not in the
>     business of sweeping isomorphisms under the rug.

Thanks, Andrej, for trying to clean up the discussion!

Thorsten hads not daid how to inetrpret equality. In an arbitrary
topos there is no other choice than interpeting equality by fibrewise
diagonals. So we have extensional equality!

I am afraid there want exist too many univalent categories. They all
would be rigid which is very inconstructive.

Thomas