From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:aca:670a:: with SMTP id z10-v6mr16328086oix.97.1525557975371;
        Sat, 05 May 2018 15:06:15 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a9d:762:: with SMTP id 89-v6ls1325624ote.6.gmail; Sat, 05
 May 2018 15:06:14 -0700 (PDT)
X-Received: by 2002:a9d:5741:: with SMTP id x1-v6mr18009887oti.73.1525557974654;
        Sat, 05 May 2018 15:06:14 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1525557974; cv=none;
        d=google.com; s=arc-20160816;
        b=CI5z+NgI3HQbgbpxxhIJMVZZNzsqMfFzfrXFV8s20DOIcSYcJQV8Q6IpHbLEmXfHXm
         wSRhFpEMz/pSPty6uMOTdN6zd9+P5Hu6X4o8DoW7pJa96AM0993/wXhj5sG6/5PXyY2i
         Q8kpr0ibRQwHZOVP6Mtpzq9V3Mqsb7qqGYy3HytGEnJgfvqltT9JUJg1tT/W4VnAIev4
         qvRa5gBFVqXWJYj4eyCa9Fw1lS9w+vhqtFBt5PceKjBBWFV+QKlxuGlHolqtEWQnCL3q
         DUqeuibP/9WpY+b5PeCqXnRwiEFbSNaum2r2PObdrSv8huR09AK1N7r/JQRqlYa1GDbv
         LH7g==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=to:subject:message-id:date:from:reply-to:mime-version
         :dkim-signature:arc-authentication-results;
        bh=lwrzkWV3Tzpm4o7r9r8QjRlP0UydNBGcocf1CMS1ye0=;
        b=UOJplJ9BbQKCRwzQRogFKPHgJ9qr77xc9JtDWsTrkGq4v0e+9LmD319Zt/9kr5vTq3
         MJp200u3nyKA05pyNBe1C1O6O7M/Q29zFvRtoDWenQ8/SmLms+yWR0WEXIoKRbCXYsom
         Ko62OsXtN72ILuRrBfsgyoq+I2CGTyg4R7sFwZRgT9cge1rUNgBIAVa/ghmD9sQJJPke
         3UEAJKdwda6Fz7BWe+GEcYYONzwe4RLmpzQCaWSOUAjesArwhAWvwzm6g/ZK2NxQkjkc
         TVjD6GRgb8MI6GG0CE0CNXiYpbXWcd60yWF9kX6vFerDUZtR1Lcut0SkN1F46bfNyDNk
         DtPw==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       dkim=pass head...@gmail.com header.s=20161025 header.b=pW6ssMvD;
       spf=pass (google.com: domain of jamie...@gmail.com designates 2607:f8b0:4001:c0b::233 as permitted sender) smtp.mailfrom=jamie...@gmail.com;
       dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com
Return-Path: <jamie...@gmail.com>
Received: from mail-it0-x233.google.com (mail-it0-x233.google.com. [2607:f8b0:4001:c0b::233])
        by gmr-mx.google.com with ESMTPS id k189-v6si614618oif.2.2018.05.05.15.06.14
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Sat, 05 May 2018 15:06:14 -0700 (PDT)
Received-SPF: pass (google.com: domain of jamie...@gmail.com designates 2607:f8b0:4001:c0b::233 as permitted sender) client-ip=2607:f8b0:4001:c0b::233;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@gmail.com header.s=20161025 header.b=pW6ssMvD;
       spf=pass (google.com: domain of jamie...@gmail.com designates 2607:f8b0:4001:c0b::233 as permitted sender) smtp.mailfrom=jamie...@gmail.com;
       dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com
Received: by mail-it0-x233.google.com with SMTP id e20-v6so7459399itc.1
        for <HomotopyT...@googlegroups.com>; Sat, 05 May 2018 15:06:14 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20161025;
        h=mime-version:reply-to:from:date:message-id:subject:to;
        bh=lwrzkWV3Tzpm4o7r9r8QjRlP0UydNBGcocf1CMS1ye0=;
        b=pW6ssMvDnEoMcl/FiBkjjX5a5min9AUrhvoNU0+Wfqwe+CnTJ5G701PAKQaDavGrUt
         FplgU+SasyVEYWZc1MnQ5ZT0J6z6jO/3OEkvmojKhVjMsoq3kA5gw0y+BsbOTM3WEvKw
         9DI0Jq8Cie7/C1EeA7Jc33+CbJTg7LY+bRbGUGCzVTJOoQA+BKHxixEPLxDzPhvwJBd1
         Ex0QWxLDzdmyGKp+W2DYnARNKuT2lwz45GqAVf1Ri8S9nDZ1PtyrmJAdm7LTNWY6GeqU
         kEx/1QZyExILMK1dud2+DJ0F2bNB94morWsDuS0uIXfexubNwHV17WL8Cm7DUU/HXztD
         zdNg==
X-Gm-Message-State: ALQs6tBvMqQcwr2fqmnc0hirFJzZTRJcAqk0ymyYxaoPfF4JZLO/smY0
	G/PkOBOilyUtXO5B4sIhsyW+ZOSfNCwkpu6YpLIjjw==
X-Received: by 2002:a24:45a4:: with SMTP id c36-v6mr33541338itd.18.1525557974169;
 Sat, 05 May 2018 15:06:14 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.107.25.10 with HTTP; Sat, 5 May 2018 15:05:53 -0700 (PDT)
Reply-To: jamie...@gmail.com
From: Jamie Vicary <jamie...@gmail.com>
Date: Sat, 5 May 2018 23:05:53 +0100
Message-ID: <CANr23v1Q-bei4kzAvEZ1LtEiqYR5FY6OsUBVnT_wD8Ee5F1gcA@mail.gmail.com>
Subject: Eckmann-Hilton for triple loop space
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset="UTF-8"

Dear all,

The formalization of the Eckmann-Hilton argument is given in Chapter
2.1 of the HoTT book. Just to fix notation, let me recall the
statement: for any type A, and for any paths a,b:id_A->id_A, there is
a path sigma_{a,b}:a.b->b.a which reverses the order of composition.

If A is itself a loop space, it is then expected that
sigma_{a,b}.sigma_{b,a} = id. (For this to be interesting, I suppose
the sigma_{a,b} would have to be chosen as a natural family, rather
than arbitrarily.) My question is whether this standard observation
has been formalized in homotopy type theory, and if so, where.

Best wishes,
Jamie