From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.233.218 with SMTP id j87mr956530lfk.26.1493922195219; Thu, 04 May 2017 11:23:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.47.86 with SMTP id v83ls412530wmv.1.canary-gmail; Thu, 04 May 2017 11:23:14 -0700 (PDT) X-Received: by 10.28.217.143 with SMTP id q137mr216812wmg.11.1493922194168; Thu, 04 May 2017 11:23:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1493922194; cv=none; d=google.com; s=arc-20160816; b=zN0yirQtsL/zVCj5KwI7tB8M0Ygjdc7+HXE7kOVfuMpeflH3VPqMqN/lTRwRRd2iKf Kk/+R0S8TXyhCnHRYMxgvZZHigp7Yna6GfQRpMeed0opbK/hzbDrVKeNb5e/1xarJL1q UoAxEulCx2z775408IsD/P7F2h4NDlj26PFdeWflyJXDz9EwIl/b35Q4ydKjdsa3bX+S 91p2yaSB8WLz+IB36UUwa+hojF74j22XZtS8MlSge6E8tOSBTQFmp4wJ+UaQkeL45JS9 432D1cfUN5wEDiiXONwyOYHtTK4ddYgn6OZClUKkESFfEajBgGD+dQ85/81P3LegneMq +1Hg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:arc-authentication-results; bh=1QzcljKJo5FURC2FvhzI8I8ThTIoIMISDB2BWOnall4=; b=iffxEenc5PDfGGg2nBJMshp5woR1VZHbamzhxyKyNzmi2M+VjW8KafG8OeLnqORPYM oxY2qYiMThR0AGaXxvvQf0W2Ez+mUZl3AYk7Jez1FROSwJb1YShJEuemayY2W6kJTQwv Eiv/TzDggnkdo/BNciNsSsQavSCFX+YUhZowtvYBRsrYKYIxLLXzAVj/s6pP457abYUj FmxA753laFb8JabpBDQ5GRaMeg4hfMP9iyLFp2IXb0l7bbDBdhTgP0aOhOEnKQDKQ8/V wnTncjxt/3V3umZUD7Q0TEApLHjtLSPCq1qZBttHuE0tzztADlwt8O88TyF8R5/gbFzY NVlw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.138 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Return-Path: Received: from arryn.ita.chalmers.se (arryn.ita.chalmers.se. [129.16.226.138]) by gmr-mx.google.com with ESMTPS id w126si31170wmd.1.2017.05.04.11.23.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 04 May 2017 11:23:14 -0700 (PDT) Received-SPF: neutral (google.com: 129.16.226.138 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) client-ip=129.16.226.138; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.138 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Received: from tyrell.ita.chalmers.se (129.16.226.132) by arryn.ita.chalmers.se (129.16.226.138) with Microsoft SMTP Server (TLS) id 15.1.396.30; Thu, 4 May 2017 20:23:12 +0200 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.0396.037; Thu, 4 May 2017 20:23:13 +0200 From: Thierry Coquand To: homotopy Type Theory Subject: notation Thread-Topic: notation Thread-Index: AQHSxQN9rYPP8HyvxUO2mMbyGANPRw== Date: Thu, 4 May 2017 18:23:13 +0000 Message-ID: Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-exchange-messagesentrepresentingtype: 1 x-originating-ip: [129.16.10.245] Content-Type: text/plain; charset="us-ascii" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 I was told that the notation in my previous message may be confusing: I wr= ite m_c : X -> D_c(X) with X implicit argument. With X explicit argument, the notation would be m_c X : X -> D_c(X) and condition of being idempotent is that D_c(m_c X) and m_c (D_c X) are path equal. Since D_c(X) =3D X^{F(c)} this can also be expressed as the fact that X^{pi_1} and X^{pi_2} : X^{F(c)} -> X^{F(c) x F(c)} are path equal (note that F(c) is not required to be fibrant). Another way to state it as a proposition is that the multiplication of the= monad X^{diagonal} : X^{F(c) x F(c)} -> X^{F(c)} is an equivalence. Thierry