From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a9d:883:: with SMTP id 3mr13284728otf.344.1588590253258; Mon, 04 May 2020 04:04:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4d0c:: with SMTP id n12ls2471787otf.7.gmail; Mon, 04 May 2020 04:04:12 -0700 (PDT) X-Received: by 2002:a9d:75c1:: with SMTP id c1mr14409952otl.339.1588590252216; Mon, 04 May 2020 04:04:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588590252; cv=none; d=google.com; s=arc-20160816; b=jMwR5gUYF6Gb1wggy++bo+dFNjj21OOpex23dIHgXjTGOzfjij/2YuNywSRZTlgYvI aGfeFbm7q4b27Nx8AcAoc3gywjIlkYlpAKeWJRM5+gzuu8ciX1pNWb2DKld94ks4943o hwhmt3MYb9xwKx+/Am3f3Ju6QM+xlbWfcTy+qHSNo7kFyrzMo9OQkjAqXp9wQPN+RwES IRhaZW6ZHpqQ0zFRkf+ULSwkJ8cT5Pe3uneArdWFfL1i4s/B8QOuHkJU9S5y0aSb0Z32 a6kVxiMpHYqHEL74xtcOahBXC+bt9sRXcPcra1JwRU5J2cOfVKHC5OowAl2kZVWFSlH1 fNrw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:cc:references:message-id:date:subject:mime-version :from:content-transfer-encoding:dkim-signature; bh=cZbFr5xiZ5MeDFYWR2RyoInBd2grYnBBUUKKCetK/eo=; b=VMk+Eiw8BCOOd6HF+rtEzY1nfztjP1VJMPK37hgRA62TTCfP0FF+6uY+Hy9zJuBEwW /Lrw53v7n9Jl3XSp15UTbRQacrCUReDC0K/+YfP42iz7iriCR9B4Wi1RR4arAIxnjm2d zLOgL6ZnCPiVkJl685Y1LGGhZx4Nxy3ny+9Kbubm0nYRHMvzSP9BUH3ByGYLhGbYHjjx dJZhCBJdGZrmMjrVI8f40ZqPhe+CgyyBuc9FgFRlzFazjwRRe8lWSebmysboNqD9NDaI maygTnKU59FA0hRo850Y9YIP4aVcOp0ikmL5xA7IoSRieqmH0LL+prfhuGPIvVluxZgf t21A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=XjELuEyk; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::82e as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt1-x82e.google.com (mail-qt1-x82e.google.com. [2607:f8b0:4864:20::82e]) by gmr-mx.google.com with ESMTPS id i22si487563oib.2.2020.05.04.04.04.12 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 04:04:12 -0700 (PDT) Received-SPF: pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::82e as permitted sender) client-ip=2607:f8b0:4864:20::82e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=XjELuEyk; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::82e as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qt1-x82e.google.com with SMTP id s30so13555388qth.2 for ; Mon, 04 May 2020 04:04:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=content-transfer-encoding:from:mime-version:subject:date:message-id :references:cc:in-reply-to:to; bh=cZbFr5xiZ5MeDFYWR2RyoInBd2grYnBBUUKKCetK/eo=; b=XjELuEykyArMvlRUNQMZ95C1fz7Xfj8e1fbsFi65aNAoFUbS+BxMWSoSgM9yWCf3Sg 6h2k2S5tej8s0k/dCTAaaDLNT1InjnJrclhNGtf1eIiIB9iMKTtyN7+KR2vNcs0gWukT hJ2jMBAaAxU+XWWnzfZGPsgwuUCDxdeD5QEvgQIMoxpMOWaqX8j4xYgXMTh9vCqjHvd2 2ZW21OvuDQjwVzcGq7ocH1io6zlyFz5RlQRq9wj9G2Fjnldc6RavXaEUEMl57BbVjpX+ aLkn31hmHYwnzTmcpvZfvv3/H/1v6LDNbLL5t2qawuYU8p/0BS3H+sZBMC5lnAsZg0X4 7bRw== X-Gm-Message-State: AGi0PuYfdPUkMw1RwOJqPowg4qpXpRgFwUlFBz3XDDFV1yLhLg64/tdj +yIZZ/SfbgXryuqRL0oIj/0TGLhzRaY= X-Received: by 2002:ac8:90c:: with SMTP id t12mr16232030qth.12.1588590251674; Mon, 04 May 2020 04:04:11 -0700 (PDT) Return-Path: Received: from [192.168.1.152] (pool-74-111-173-45.pitbpa.fios.verizon.net. [74.111.173.45]) by smtp.gmail.com with ESMTPSA id e24sm9677280qkl.56.2020.05.04.04.04.10 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 04:04:10 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable From: Steve Awodey Mime-Version: 1.0 (1.0) Subject: Re: [HoTT] "Identifications" ? Date: Mon, 4 May 2020 07:04:09 -0400 Message-Id: <958244CE-832E-4DF7-8A83-A98D70D59193@gmail.com> References: Cc: Thorsten Altenkirch , "homotopyt...@googlegroups.com" In-Reply-To: To: stre...@mathematik.tu-darmstadt.de X-Mailer: iPhone Mail (17D50) This terminology was first proposed by Dan Grayson in one of our discussion= s in Simonyi Hall, as a way of understanding the elements of identity types= . It=E2=80=99s used occasionally in the book.=20 Regards, Steve=20 > On May 4, 2020, at 06:59, stre...@mathematik.tu-darmstadt.de wrote: >=20 > =EF=BB=BF >>=20 >> I am just reading a paper which uses the word =E2=80=9CIdentification=E2= =80=9D instead >> of equality. I think this has been proposed by Bob Harper. Can anybody >> enlighten me what is the difference between identifications and equality= ? >> Maybe there is an identification between them but they are not equal? Ar= e >> the real numbers 0.999=E2=80=A6 identified or are they equal? >=20 > You may identify things which are not equal. So ''identify'' seems to mea= n > consider as equal. > In a sense this is very descriptive for what is going on in HoTT where on= e > never performs quotients but rather widens equivalence relations. > 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. >=20 > Thomas >=20 > --=20 > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/f23c7b1ada3c6fd99e47a70620c9e278.squirrel%40webmail.ma= thematik.tu-darmstadt.de.