From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:600c:210c:: with SMTP id u12mr14716699wml.135.1588589971193; Mon, 04 May 2020 03:59:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:f6c4:: with SMTP id y4ls21027477wrp.2.gmail; Mon, 04 May 2020 03:59:29 -0700 (PDT) X-Received: by 2002:adf:f4cb:: with SMTP id h11mr19500741wrp.191.1588589969861; Mon, 04 May 2020 03:59:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588589969; cv=none; d=google.com; s=arc-20160816; b=nAdKmwCu1fd8VoSeA3zXI7LdTDOoim1mBN5Nf0lB/ieBGaMQfHK9M981+vkeHUA1wl tH8qz5xyQ+AMhHUb9pyHEgHseH1J6pGKa3jIvsCTmfn8ByUPVmrt6n1GHXRvuX+7yJwC uQnaQNU8OWu7La13jbG5h1voKTLmZjWcNKwW6XlpxoifgEJimRrQ+gUkh/rccPtlsswX T+BuOijMBbUhtWYcy5lsqyPAb6BMPw4H9dAUOQIvrROxNhqpl0HMNQvoEEiCYCj8kzDd 9NIwDXjsh6lSDwkkJ2LI2i5/1Xbi7B+e7N7HUAI9maiPrluQdfZBGMLzY/ZFzmswqp9a irog== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=importance:content-transfer-encoding:mime-version:user-agent:cc:to :from:subject:date:references:in-reply-to:message-id; bh=zeHIUWqdngKvkPnZrvcIfQeRXwisifziO3MjkdIC4sE=; b=bW0/2+MeGnFRjf6enzQOx2axZ1VqKD5kZYlv4ACnIgKc6jBStSA4sJdwisbyVpXjZq NVYt/RrcIWaqO2cBToFxwGEIhMBuNAtM2DF11x/2FsZv/EmnRh3Gz1sp1uvGUkEcOlUU wwgLiqKAcouAqa4P7D0m3kuYywn9ixW5oWSNRxHxX70GH43NchTeFK0yJ/6L7Eh3qosZ 2KmtobG0JeEamEtlZxO4WDkYL11beNmkQJrHQjcORJfdahDkcmcuEWLQeo0G8RIysLj/ hPSG/iQjtAvz/sMXbf5po+sSWKavQN2/gORxScOhkotNBKc6opGIpQ2H8dhMqzhEIomx Owag== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from mail-relay232.hrz.tu-darmstadt.de (mail-relay233.hrz.tu-darmstadt.de. [130.83.156.233]) by gmr-mx.google.com with ESMTPS id q18si232931wrc.3.2020.05.04.03.59.29 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 03:59:29 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) client-ip=130.83.156.233; 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.233 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]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mail.mathematik.tu-darmstadt.de", Issuer "DFN-Verein Global Issuing CA" (verified OK)) by mail-relay232.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49G0H451T1z43p8; Mon, 4 May 2020 12:59:28 +0200 (CEST) Received: from webmail.mathematik.tu-darmstadt.de (fb04277.mathematik.tu-darmstadt.de [130.83.2.17]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id 044B015C008721; Mon, 4 May 2020 13:00:01 +0200 Received: from 79.233.167.171 (SquirrelMail authenticated user streicher) by webmail.mathematik.tu-darmstadt.de with HTTP; Mon, 4 May 2020 12:59:28 +0200 Message-ID: In-Reply-To: References: Date: Mon, 4 May 2020 12:59:28 +0200 Subject: Re: [HoTT] "Identifications" ? From: stre...@mathematik.tu-darmstadt.de To: "Thorsten Altenkirch" Cc: "homotopyt...@googlegroups.com" User-Agent: SquirrelMail/1.4.21 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal > I am just reading a paper which uses the word “Identification” 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? Are > the real numbers 0.999… identified or are they equal? You may identify things which are not equal. So ''identify'' seems to mean consider as equal. In a sense this is very descriptive for what is going on in HoTT where one 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. Thomas