From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.157.24.87 with SMTP id t23mr1466088ott.104.1476353646977;
        Thu, 13 Oct 2016 03:14:06 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.157.56.29 with SMTP id i29ls5053996otc.12.gmail; Thu, 13 Oct
 2016 03:14:06 -0700 (PDT)
X-Received: by 10.129.74.215 with SMTP id x206mr1685622ywa.93.1476353646440;
        Thu, 13 Oct 2016 03:14:06 -0700 (PDT)
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx503.hrz.tu-darmstadt.de (lnx503.hrz.tu-darmstadt.de. [130.83.156.232])
        by gmr-mx.google.com with ESMTPS id p70si1565597vkd.0.2016.10.13.03.14.05
        for <HomotopyT...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Thu, 13 Oct 2016 03:14:06 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.232 as permitted sender) client-ip=130.83.156.232;
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.232 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 u9DAE3qc025516;
	Thu, 13 Oct 2016 12:14:03 +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 u9DAE370003554;
	Thu, 13 Oct 2016 12:14:03 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 1C4021A3F4E; Thu, 13 Oct 2016 12:14:03 +0200 (CEST)
Date: Thu, 13 Oct 2016 12:14:03 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Martin Escardo <escardo...@googlemail.com>
Cc: Vladimir Voevodsky <vlad...@ias.edu>,
        Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>,
        =?iso-8859-1?Q?Joyal=2C_Andr=E9?= <joyal...@uqam.ca>,
        "HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence
Message-ID: <20161013101402.GB6783@mathematik.tu-darmstadt.de>
References: <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com>
 <25c7daf7-8c0f-97de-7d3d-34851bf50a98@googlemail.com>
 <cb48b96b-1dc6-fc80-51c9-c6293d4fd4dc@googlemail.com>
 <8C57894C7413F04A98DDF5629FEC90B138BCC04E@Pli.gst.uqam.ca>
 <afe2cdaf-c634-900a-7461-efe10aced914@googlemail.com>
 <8C57894C7413F04A98DDF5629FEC90B138BCCE8B@Pli.gst.uqam.ca>
 <ef07b4b0-db2b-0639-1340-6fc9ce479dd6@googlemail.com>
 <CAAkwb-nX167c_hpd2pE7d5VWQ+q30sKJs2V8zf=yEqDpiuL2mw@mail.gmail.com>
 <CBA53C75-423D-4E98-9C59-BE98166A8FB4@ias.edu>
 <99874c3d-46e7-cf41-e58e-63183ae10d74@googlemail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <99874c3d-46e7-cf41-e58e-63183ae10d74@googlemail.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: 2016.10.13.100316
X-PMX-RELAY: outgoing

> I do find it rather interesting that the cartesian product of two such types
> that are not in general hpropositions is always an hproposition.

Well, it rarely happens that li(f) and ri(f) are both inhabited and if
so then both contain morally just one element (in case of Set).
The point seeeems to be that the type li(f) x ri(f)  is connected. If
you intersect it with the diagonal then it is not connected anymore.

That subobjects of connected objects need not be connected anymore is
geometrically quite intuitive.

For example (\Sigma y:A) Path_A(x,y) is always connected though its
subobject Path_A(x,x) is not.

Thomas