From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:600c:20c:: with SMTP id 12mr15455675wmi.91.1588592550973; Mon, 04 May 2020 04:42:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:1f0e:: with SMTP id f14ls18331715wmf.0.gmail; Mon, 04 May 2020 04:42:29 -0700 (PDT) X-Received: by 2002:a7b:c5d4:: with SMTP id n20mr14886698wmk.92.1588592549709; Mon, 04 May 2020 04:42:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588592549; cv=none; d=google.com; s=arc-20160816; b=I9KGXLJVUx2R0/aoBV14pyzi0fD2rEIhOKEY5bu5ETQO1CrjfNukn5Bu9mgOwvl58c NmKvbohQxzz/VMym6AiML4oSNlEuLi/V13urqZxYNGLdTzkFQ9VtpCsFKjKTVPydKFrZ lAXgoLlFt6dhtuxrrjaGgZZq0SCHNJDMQnSw3tlAGf7dqTtIBWKsNGcmW6bOLwIcyBJE R2hSEc4fywlB1Gar1589ebfO1nt6x+JKQNK/kKkRkIv/+wVbQBbuE5RfSZXUS2KebHEK cD/bv6NGqvw3AeAV5Popk3EwayostqSkp5+P0lsu/0btUiXPprRLw6Lcxxg3HkMt8iW9 VRCw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature; bh=CGYkkVWYjW26Op1SztWcDzsF1Z4muf2dGu0DEMZ/v2I=; b=HnzanmGa8SHVU5F1zDe9mFztVZDtjK7VsI6H1YFxazPMdsA/XAineMJxSxfcnyahSq SsmMJi6UpTycM6PDT5y8gue0bJz3z3EiayU63nqr1ELrqcGJMhZNtgmddSCX6DgdyEv0 BfFi1hKbk9poC/uwR1GdUU+Zd56NgYsNrp/n8rUSXApPFackB8wvyZpGMw0IKCCkFyAk we8JcP+elwtcCXvaUOPJ5tGsSqi1U8NL1oaVrsKLwHQW+P7u439b1EHOF1q9UNYaDXOp TEXc6HWvhgZ86tNpgGtqD7NonZADK8jR9/mRRXFU+k9ZR35h5mgSSnM4cSZ2AwJ2d1ad Ul8Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=nDWFdy6T; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::332 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm1-x332.google.com (mail-wm1-x332.google.com. [2a00:1450:4864:20::332]) by gmr-mx.google.com with ESMTPS id 71si1276277wmb.1.2020.05.04.04.42.29 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 04:42:29 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::332 as permitted sender) client-ip=2a00:1450:4864:20::332; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=nDWFdy6T; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::332 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wm1-x332.google.com with SMTP id r26so8661975wmh.0 for ; Mon, 04 May 2020 04:42:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding:content-language; bh=CGYkkVWYjW26Op1SztWcDzsF1Z4muf2dGu0DEMZ/v2I=; b=nDWFdy6TAYKoh8nXOVDqGas3LNLzYUv1b64o/nUzMCWEX8eDtwG9VQYdfaXDO6m0en KttP86kz41j5RJPWJ9EVyRqFeketPlJf1kz5ldqlkPHXdWiKOgpy3XjqX+Tgclgg60t2 sUy5ZIB9dD0oWCWP6W7VlEXBcm16qbHiGG8HQ2UB47x3iePYj6WIYPXzEqNBSpuW0Ul5 pXNzLiOlydRQIhscrIxKm3MFvth3vCXPYLGwt7P2Y6GgIYVLzBOf2wjQ5jHD3aPLpNeT ExqzU3sJRHm0Z3R00hMq/Qp0o+OM8QyPXUq2qR5+wCXg4o1VE5yHkufl3n19yPTCHhFM gYxg== X-Gm-Message-State: AGi0PuanF2BSqDpP59T472TUIdtgbn/pOaqZaztE9H8pgTrcBxxiKwyP R4PCsDgTm0nJqJS16YDRDfPjvT7kOqM= X-Received: by 2002:a1c:a344:: with SMTP id m65mr14196785wme.20.1588592549167; Mon, 04 May 2020 04:42:29 -0700 (PDT) Return-Path: Received: from [192.168.1.67] (37.67.90.146.dyn.plus.net. [146.90.67.37]) by smtp.gmail.com with ESMTPSA id f23sm12472266wml.4.2020.05.04.04.42.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 04:42:28 -0700 (PDT) Subject: Re: [HoTT] "Identifications" ? To: HomotopyTypeTheory@googlegroups.com References: From: Nicolai Kraus Message-ID: Date: Mon, 4 May 2020 12:42:27 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US On 04/05/2020 12:17, Thorsten Altenkirch wrote: > This is really different in the respective topos models as eg simplicial > sets or already the topos of reflexive graphs as exemplified by N. Kraus's > puzzling counterexample. > > What puzzling counterexample is this? Thomas was referring to: https://homotopytypetheory.org/2013/10/28/ You may also have seen it in my thesis or the paper "Notions of Anonymous Existence in Martin-Löf Type Theory". :) Nicolai