From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.12.133 with SMTP id 5mr1647623pfm.15.1508083236847; Sun, 15 Oct 2017 09:00:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.98.2.206 with SMTP id 197ls2803566pfc.7.gmail; Sun, 15 Oct 2017 09:00:35 -0700 (PDT) X-Received: by 10.99.39.65 with SMTP id n62mr1630246pgn.121.1508083235700; Sun, 15 Oct 2017 09:00:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508083235; cv=none; d=google.com; s=arc-20160816; b=mMyYPAhgZ9qeR2jFHNcpPqCbUj6bjGX1uV1M5E1n4oHgmvV1p5L/RQR3JxT6qlqoEC lZ3+5pNilHZCJg2y30CPvtD7Vyh+ZlJnZAahhTVJ4ku5s/E1sQstzbwGdm3ew4MXQyEF E1AVrneOFP/EJIs7kb6sm/lgTXkyHIGkoM/Z3sYunINqfXM/a3QTrQeiBLMqQhEGHYxD M+NapFzhoYzCxmiAh1IzDd7rDoGTWmxmcGNSRItMCYL34tXUSgVwiWdfQxgfrnbsC+aR OEfFnJSQvneziV66Oou2flJfUgoQja19H17yUqF2DwRP61MifF9Yosqnm1kTRQllMau/ R0hA== 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=LsxC6hITqGJGdFSo+mHdJ78VxijUw7/tCCdzEuE4l8Y=; b=fuZpkKOs/GKfFE/iDIJSoxak8N0KFo4BbVOEwaWafMUi3HrlTpM26mvakHxcdHitBb EGCoat2TS/wBA7XM6UX9OnwLa67Ib7FklQGykZsgtjjTbRPFMghC/GoaJXXd5tLAQ12+ gfxO83SuT2L6JTTsY2Ui9MHLOBov35+L51zDh1WKSwMq7U8mGTYffp/twG73WUaYeWwp HAO7CvXNOlZtgR3Vlwv09JmeGmJ7yT3yTOIiAgvF84iZO+N3H9ISvZuojqxLoplJMl7L SKu9CnyyIWTi+SZSz0FiN9vtBHTrhT16koGMs45Qx94ZXr38NwEt64QS5XsmJ94kq8G5 7A5g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=MP11jpK7; spf=neutral (google.com: 2607:f8b0:400d:c0d::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x232.google.com (mail-qt0-x232.google.com. [2607:f8b0:400d:c0d::232]) by gmr-mx.google.com with ESMTPS id a24si208163pfc.5.2017.10.15.09.00.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 09:00:35 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::232 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=MP11jpK7; spf=neutral (google.com: 2607:f8b0:400d:c0d::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x232.google.com with SMTP id 31so1964385qtz.9 for ; Sun, 15 Oct 2017 09:00:35 -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=LsxC6hITqGJGdFSo+mHdJ78VxijUw7/tCCdzEuE4l8Y=; b=MP11jpK7BSxa1DgDrHqgO3HZT1K+tXV88jANN7zvnH/G2t1sFYjV0nybaWI3UiIyBE mNpQ4clC7EvG3NIssiTGBFZNk8k9s7dFNFViONAfDZo2btF3xdeOdk1jIZCcPwYlCUdG UW3pY9s6it3niBmyi13bbRLhHB7T/cNAJbPVnQ5YjCjeSAPac+pPZK6TVeKlsnpyQ/M2 JS4T4pJTQVw5z1p/CYQNSQIpO6bJKq24CkqLszn7b39OZ+lq4p2cpmBQSl7dq+OLQVJo Eb/W0t1tGa49JggVMS7zff0ttPVgBt9gHW1YG4TDBioscgVdIA55rab/3vunbbZg+Fgr JJ6Q== X-Gm-Message-State: AMCzsaVxckoUsqPpJe4vqyGEiWlI5t8IsGiUgDSpFLL+Y6ZyNUl76w3H 37hkogP53O0R885u7277+ircgygt X-Received: by 10.37.187.75 with SMTP id b11mr4844402ybk.445.1508083235140; Sun, 15 Oct 2017 09:00:35 -0700 (PDT) Return-Path: Received: from mail-oi0-f42.google.com (mail-oi0-f42.google.com. [209.85.218.42]) by smtp.gmail.com with ESMTPSA id q125sm2434437ywg.22.2017.10.15.09.00.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 09:00:34 -0700 (PDT) Received: by mail-oi0-f42.google.com with SMTP id h6so1000782oia.10 for ; Sun, 15 Oct 2017 09:00:33 -0700 (PDT) X-Received: by 10.157.19.71 with SMTP id q7mr4427658otq.172.1508083233420; Sun, 15 Oct 2017 09:00:33 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Sun, 15 Oct 2017 09:00:12 -0700 (PDT) In-Reply-To: References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> <20171015074530.GA29437@mathematik.tu-darmstadt.de> <20171015135740.GA7845@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Sun, 15 Oct 2017 09:00:12 -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" I mean, it seems to me kind of like the difference between proving a type A is contractible by Sigma(a:A) Pi(x:A) (x=a) and by A x Pi(x y:A) (x=y) i.e. not much. But maybe I am missing something? On Sun, Oct 15, 2017 at 7:53 AM, Michael Shulman wrote: > I'm not saying to do anything different mathematically, just to > *think* about "using a partial interpretation function on prejudgments > and showing that all derivable judgments get a meaning" as *being a > way of* "assigning meanings to derivations and showing that distinct > derivations of the same judgment get the same meaning". > > On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streicher > wrote: >>> > 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? >> >> In principle yes but it is very laborious. First of all you have to >> formalize derivations and do a double induction on them which I don't >> know how to to perform. >> >> 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.