From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.28.209.203 with SMTP id i194mr879990wmg.4.1473678866031;
        Mon, 12 Sep 2016 04:14:26 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.197.136 with SMTP id v130ls1307528wmf.14.canary; Mon, 12
 Sep 2016 04:14:25 -0700 (PDT)
X-Received: by 10.28.198.133 with SMTP id w127mr1594458wmf.3.1473678865263;
        Mon, 12 Sep 2016 04:14:25 -0700 (PDT)
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx503.hrz.tu-darmstadt.de (mail-relay15.hrz.tu-darmstadt.de. [130.83.156.239])
        by gmr-mx.google.com with ESMTPS id b1si261189wmg.0.2016.09.12.04.14.25
        for <HomotopyT...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Mon, 12 Sep 2016 04:14:25 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239;
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.239 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])
	by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id u8CBELQT020524;
	Mon, 12 Sep 2016 13:14:21 +0200
	(envelope-from stre...@mathematik.tu-darmstadt.de)
Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209])
	by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id u8CBEL70007040;
	Mon, 12 Sep 2016 13:14:21 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id 3563F1A5675; Mon, 12 Sep 2016 13:14:21 +0200 (CEST)
Date: Mon, 12 Sep 2016 13:14:21 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Andrej Bauer <andrej...@andrej.com>
Cc: Martin Escardo <escardo...@googlemail.com>,
        "HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Meta-conjecture about MLTT
Message-ID: <20160912111420.GA14499@mathematik.tu-darmstadt.de>
References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com>
 <CAB0nkh2eZT+yOVDmdxPdkg2iKuvJFU2W=Qd_MmM1=CW9tFrDNw@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <CAB0nkh2eZT+yOVDmdxPdkg2iKuvJFU2W=Qd_MmM1=CW9tFrDNw@mail.gmail.com>
User-Agent: Mutt/1.5.23 (2014-03-12)
X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2016.9.12.110617
X-PMX-RELAY: outgoing

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
>