From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.207.131 with SMTP id f125mr1608186wmg.4.1473679391626; Mon, 12 Sep 2016 04:23:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.32.207 with SMTP id g76ls112499lji.42.gmail; Mon, 12 Sep 2016 04:23:10 -0700 (PDT) X-Received: by 10.46.0.14 with SMTP id 14mr2497716lja.8.1473679390903; Mon, 12 Sep 2016 04:23:10 -0700 (PDT) Return-Path: Received: from mail-lf0-x22b.google.com (mail-lf0-x22b.google.com. [2a00:1450:4010:c07::22b]) by gmr-mx.google.com with ESMTPS id e21si787082wmc.2.2016.09.12.04.23.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 12 Sep 2016 04:23:10 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::22b as permitted sender) client-ip=2a00:1450:4010:c07::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2a00:1450:4010:c07::22b as permitted sender) smtp.mailfrom=andrew....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22b.google.com with SMTP id u14so84414646lfd.1 for ; Mon, 12 Sep 2016 04:23:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=DrKxBEFHi60h1x62w4kIail4b+hVdrYWt1TzY9G83bg=; b=qJY4/5JbovlGPTxR2E+iEXu0XPA/z9l77UZEKg1IoAYdM9vWV0+freVQjKqoRGIn0n LUQqGm9SIextHeZRgpKV584wtFL6jVNq0TkEifQh2qCYPntS9Vy1Y6U4sZdIwlHmmoyI rySOjxdQ9BzsXX663zSQvdchcHD74ynTqXS8wdRBT+lM/6tXvlwSfy3YmKnGlRO9El3x utnkTrTZohlxcF2ppVyj94utN5cv9dQLOH3rRV+ASkPt5MoTBqF2jUNo8I/56yK56EeH MEO7TLy8nQOxGWRnBPEVJy9LQ3dlmUSKDXHhd7MZVH4iUinQilMYeyAh9FrUCGH3dav0 C3tQ== X-Gm-Message-State: AE9vXwOfeEFB9FIKBzdPufObeK6KL/UJ0BMOivRs0JNj7wk2LE+PshM8Avdu8gfZsh89bS2x4vhwFp2/tGu8Kg== X-Received: by 10.25.38.149 with SMTP id m143mr5936550lfm.107.1473679390539; Mon, 12 Sep 2016 04:23:10 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.83.143 with HTTP; Mon, 12 Sep 2016 04:23:09 -0700 (PDT) In-Reply-To: <20160912111420.GA14499@mathematik.tu-darmstadt.de> References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> <20160912111420.GA14499@mathematik.tu-darmstadt.de> From: Andrew Polonsky Date: Mon, 12 Sep 2016 13:23:09 +0200 Message-ID: Subject: Re: [HoTT] Meta-conjecture about MLTT To: Thomas Streicher Cc: Andrej Bauer , Martin Escardo , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 Perhaps one does not need to take a skeleton. A dependent type x:U |- P(X) : Type gives rise, in the *standard* set-theoretic model, to a family of sets indexed by [[U]]. Since the standard type constructor preserve isomorphism, two fibers [[P(A)]] and [[P(B)]] will be isomorphic if A and B are. Saying "A provably has property P" translates into "[[P(A)]] is inhabited by a definable element". In principle, one could conceive that [[P(B)]] has no definable elements, even if the two are isomorphic. But saying that "B provably does not have property P" translates into "[[P(B)]] is empty", which cannot be the case. Cheers, Andrew On Mon, Sep 12, 2016 at 1:14 PM, Thomas Streicher wrote: > I am afraid this skeleton model is not split and spliiting it it wan't > be a skeleton anymore. > > Thomas > > > On Mon, Sep 12, 2016 at 01:02:24PM +0200, Andrej Bauer wrote: >> Let me try. >> >> Consider the model of MLTT in the skeleton of sets, i.e., types are >> interpreted as cardinal numbers and functions are the set-theoretic >> functions between cardinals. The identity type is just what you'd >> expect in a set-theoretic model (in fact, there is *no* choice about >> i). There are no problems of coherence anywhere. >> >> This model validates equality reflection. If MLTT+reflection >> distinguished isomorphic types, then there would exist in this model >> two isomorphic types which are not equal, but since we started with a >> skeleton this will not do. >> >> It is a bit amusing that the model also validates things like Id(U, >> Nat -> Nat, Nat -> Bool) and is thus quite educational. >> >> It is a model, right? >> >> With kind regards, >> >> Andrej >> > > -- > You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/_cgjnmRvcUU/unsubscribe. > To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.