From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.52.154 with SMTP id w26mr5434892qtb.36.1508062391367; Sun, 15 Oct 2017 03:13:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.55.39.11 with SMTP id n11ls141325qkn.13.gmail; Sun, 15 Oct 2017 03:13:10 -0700 (PDT) X-Received: by 10.55.221.196 with SMTP id u65mr5364367qku.18.1508062390879; Sun, 15 Oct 2017 03:13:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508062390; cv=none; d=google.com; s=arc-20160816; b=lIuLLsYhjMqZZ9xnRssB/au8xeLgBttoA9dYch83UXSx2f6daNqMfp4edyb1H+uf1O tHqa3Z6AHSVXvQ5TkNwFTy+ifgLo4QsTy+MDpzHCjvOnBQUXAxWkfK8cxsu416qVPvtW UJb1tR/D9Py/uNrxc8/Mxkrp5TMfA8vtlC1JPiOswKnWZbBJviNjQWGUKvaOkJeXbDmj Ff//QRztP598s3lirOB832ydpa89rytJ/4dOjn+uHWruBUIoCiqtHzc9vOviRae9x7db akYfuHEMSbQDUrYO4fgw1EFO3mlPU+65hI/oG9E13BpgkXmp2hRgUFCPL9AYtKJhBs/5 ft5A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=HszsGAbkdJyLuNdWxEdcpyT3EOyCFGeIzIIOr+GVgoc=; b=drns95qhgcFX3weSV9CR+ug1e2D7GdlGnZ/ZHZ0kZdv8gSY6bvBiiGEiuj2xF1QMhW 1cVQkHYjR1ydGt07HRsDQioPoWlEofJJCQDqlDibqNduZfV0qWrMNlkfnCZ4ozDgNJEY CY/yf4gnrNHLHV/+1PnVtAOkcyGSHH3H+ni72qGxs1fZzCTTvqz/1bGUvKS0ZNV1byjy HIPiCpt28G8AUXGzMn08vndpyRN+MI7nR9YsLl4+w1nG5ozAMX1DsGa0ilO6icu25l9Y tw4Z2jqjqlXnRL/hd0u4kZqVztTuOVSx3T76NqCbcFClRMFXxt1COgA1YvwFK4KQpLdn 7PNA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=A1jOZ7t1; spf=neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x22e.google.com (mail-qt0-x22e.google.com. [2607:f8b0:400d:c0d::22e]) by gmr-mx.google.com with ESMTPS id d142si266319qke.0.2017.10.15.03.13.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 03:13:10 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=A1jOZ7t1; spf=neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x22e.google.com with SMTP id 31so1216203qtz.9 for ; Sun, 15 Oct 2017 03:13:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=HszsGAbkdJyLuNdWxEdcpyT3EOyCFGeIzIIOr+GVgoc=; b=A1jOZ7t1DEYFmaZc8xk4PtXesI0wP7aqFfhyngBHwDVousW24xrr8Wcnej+27tKvYi 9oaIRYzow1rXHyKnxNMiQIIf+wpZz+WASlrz84IvSJHQqQCQMD2Z2V1sGC89z+Ol02La hiVWD+rIrJXzWb/QHAzoZBzpKjMF0CvOhfHPEqVcURCD96L6qrfIm/el0c0zOxNVG+fw 4/1N7SgZ1GOiR7E1uTkUqImOliEa9p9ToJwXx1bYX0fUt3yl0MahO9qmED/zfQpcOf+y kEvaakGh1aQ0u6lrZJj4BlU/Rocasf+li6NODTruS+364pHZzwYiqTjrjfEkJwxyZtzH icmg== X-Gm-Message-State: AMCzsaXW1vNokKRrdEVX/mK6r9KV1zHWi/kNzsv+yIfoIDyUeFWl6EwT 4LMFZGYxenR6ljhqj9GkBXBMkZJw X-Received: by 10.13.253.134 with SMTP id n128mr4073458ywf.449.1508062390294; Sun, 15 Oct 2017 03:13:10 -0700 (PDT) Return-Path: Received: from mail-oi0-f43.google.com (mail-oi0-f43.google.com. [209.85.218.43]) by smtp.gmail.com with ESMTPSA id j3sm2164212ywe.80.2017.10.15.03.13.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 03:13:09 -0700 (PDT) Received: by mail-oi0-f43.google.com with SMTP id q4so20795125oic.7 for ; Sun, 15 Oct 2017 03:13:09 -0700 (PDT) X-Received: by 10.202.230.2 with SMTP id d2mr3717745oih.229.1508062389491; Sun, 15 Oct 2017 03:13:09 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Sun, 15 Oct 2017 03:12:48 -0700 (PDT) In-Reply-To: <20171015074530.GA29437@mathematik.tu-darmstadt.de> References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> <20171015074530.GA29437@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Sun, 15 Oct 2017 03:12:48 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Thomas Streicher Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" On Sun, Oct 15, 2017 at 12:45 AM, Thomas Streicher wrote: > It is certainly tempting to assign meanings to derivations and then to > show that different derivations of the same judgement get assigned the > same meaning. > When writing my thesis in the second half of the 80s I found this too > difficult and instead used an a priori partial interpretation > function assigning meaning to prejudgements. It was then part of the > correctness theorem that all derivable judgements get assigned a meaning. Couldn't one consider the latter to be a way of doing the former? > Most people have gone this way at least when they took pains to write > down the interpretation function at all. > > BTW the above allows one to show that assigning a meaning to derivations > just depends on the judgement: one jyust has to show that the meaning > assigned to a derivation of a judgement J coincides with the meaning > assigned to J beforehand. > > Thomas > > > > > > > > > > > > > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.