From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.21.15 with SMTP id s15mr1055936ljd.41.1501964829658; Sat, 05 Aug 2017 13:27:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.194.133 with SMTP id s127ls502461wmf.6.gmail; Sat, 05 Aug 2017 13:27:08 -0700 (PDT) X-Received: by 10.28.109.146 with SMTP id b18mr929401wmi.30.1501964828448; Sat, 05 Aug 2017 13:27:08 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1501964828; cv=none; d=google.com; s=arc-20160816; b=rwwUsIL8lkMSiBtDzynCkggPLtnRkkTAV2SMLWxOIyUuw6F9upgTHDjBIg1SuuPBt5 jfBnua4DStCAyhlpYNjmx4wdYI6h1CP+lvT4NsnIbh1J6/Q3Fba7w89+LP9/brpbH/SW RWeXWjBVaXSNuU7Joxy6DZ1Dow/NluJvTVt1jnNr6T1HH0BjBpz+KMZl3LvApiOYEXZJ lq1owalwel6Ya3it/8aR4s+CN0S0Isocv4K2mT5y+mkOtNb8xNGCNWfgrfVqsys+aeZb OB6dEYr42PDz7hN+XzTPrVlgpq9dFvTjT1nxS2IbxGyqlSQwUckdVLYUVDfAKTKmr+D5 Uuew== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:subject:from:to:arc-authentication-results; bh=w7dWjJyjhM00Kw1fY1Vch5ew+t5KZJqUrBxjaIDu7Lg=; b=XaFLe7MuVMQyBHEWgvN2UwQi7PKlwTOvvBzeHr0WSgEJ20uB+EckfDYP1Cz45Sv7C6 /+lNIi5S6khOc6fqtdzmzgypurSQ8swTMssHxe1iK+/3LsM+kaORliCkwtc2/ZLiwW64 EXxgKt+Bwk2UV2kdmOL4qMJewYlI9Mr4qJBqbJc2sFQR4xE3ks5tKvTt+dSiK3gH98zP s8QvgZMtZpqckYKDhHlYmhy7+KBZ61m9I62ceKI1Lkl65IxRocENSP+SNypu1kkID20M qTv2izaILCam9Si//xzbb+VZ9QVxKRSXXJh80fhVN3LJOVZlQQc38FxmmjTJE2luV6LV mgvg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of palm...@math.su.se designates 2001:6b0:5:1214:250:56ff:fe94:30c3 as permitted sender) smtp.mailfrom=palm...@math.su.se Return-Path: Received: from mail-prod-route04.it.su.se (mail-prod-route04.it.su.se. [2001:6b0:5:1214:250:56ff:fe94:30c3]) by gmr-mx.google.com with ESMTPS id t129si3347551wmt.2.2017.08.05.13.27.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 Aug 2017 13:27:08 -0700 (PDT) Received-SPF: pass (google.com: domain of palm...@math.su.se designates 2001:6b0:5:1214:250:56ff:fe94:30c3 as permitted sender) client-ip=2001:6b0:5:1214:250:56ff:fe94:30c3; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of palm...@math.su.se designates 2001:6b0:5:1214:250:56ff:fe94:30c3 as permitted sender) smtp.mailfrom=palm...@math.su.se Received: from e-mailfilter02.sunet.se (e-mailfilter02.sunet.se [IPv6:2001:6b0:8:2::202]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail-prod-route04.it.su.se (Postfix) with ESMTPS id 3xPwLz44hkz12RR for ; Sat, 5 Aug 2017 22:27:07 +0200 (CEST) Received: from smtp.su.se (mail-prod-smtp01.it.su.se [IPv6:2001:6b0:5:1213:250:56ff:fe94:3d10]) by e-mailfilter02.sunet.se (8.14.4/8.14.4/Debian-4+deb7u1) with ESMTP id v75KR77C018461 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO) for ; Sat, 5 Aug 2017 22:27:07 +0200 Received: from Eriks-Palmgrens-MacBook-Air.local (c80-216-1-129.bredband.comhem.se [80.216.1.129]) (Authenticated sender: epalm) by smtp.su.se (Postfix) with ESMTPSA id 3xPwLz0BtRz10Mb for ; Sat, 5 Aug 2017 22:27:06 +0200 (CEST) To: homotopytypetheory From: Erik Palmgren Subject: Preprint available: On equality of objects in categories in constructive type theory Message-ID: Date: Sat, 5 Aug 2017 22:26:49 +0200 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.2.1 MIME-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Language: sv Content-Transfer-Encoding: 8bit X-Bayes-Prob: 0.0001 (Score 0, tokens from: outbound, outbound-su-se:default, su-se:default, base:default, @@RPTN) X-Spam-Score: -0.10 () [Tag at 7.50] T_RP_MATCHES_RCVD:-0.1 X-CanIt-Geo: ip=80.216.1.129; country=SE; region=Stockholm; city=Stockholm; latitude=59.3600; longitude=18.0009; http://maps.google.com/maps?q=59.3600,18.0009&z=6 X-CanItPRO-Stream: outbound-su-se:outbound (inherits from outbound-su-se:default,su-se:default,base:default) X-Canit-Stats-ID: 0aTRwr72M - b5fc8c13c2e5 - 20170805 X-CanIt-Archive-Cluster: PfMRe/vJWMiXwM2YIH5BVExnUnw Received-SPF: neutral (e-mailfilter02.sunet.se: 80.216.1.129 is neither permitted nor denied by domain palm...@math.su.se) receiver=e-mailfilter02.sunet.se; client-ip=80.216.1.129; envelope-from=; helo=smtp.su.se; identity=mailfrom X-Scanned-By: CanIt (www . roaringpenguin . com) Here is a new note that might be of interest to the readers of the list. Whether to impose equality on objects in categories, and what kind, is an issue that becomes pressing in the formalization of models of Martin-Löf type theory inside the theory itself. On equality of objects in categories in constructive type theory Erik Palmgren Abstract In this note we remark on the problem of equality of objects in categories formalized in Martin-Löf's constructive type theory. A standard notion of category in this system is E-category, where no such equality is specified. The main observation here is that there is no general extension of E-categories to categories with equality on objects, unless the principle Uniqueness of Identity Proofs (UIP) holds. We also introduce the notion of an H-category, a variant of category with equality on objects, which makes it easy to compare to the notion of univalent category proposed for Univalent Type Theory by Ahrens, Kapulkin and Shulman. Link to preprint: http://staff.math.su.se/palmgren/eobcat.pdf