From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.157.19.17 with SMTP id f17mr15454747ote.33.1473678147758;
        Mon, 12 Sep 2016 04:02:27 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.36.105.148 with SMTP id e142ls3065069itc.17.canary; Mon, 12
 Sep 2016 04:02:25 -0700 (PDT)
X-Received: by 10.66.231.104 with SMTP id tf8mr15323455pac.15.1473678145902;
        Mon, 12 Sep 2016 04:02:25 -0700 (PDT)
Return-Path: <andrej...@andrej.com>
Received: from mail-qk0-x229.google.com (mail-qk0-x229.google.com. [2607:f8b0:400d:c09::229])
        by gmr-mx.google.com with ESMTPS id w132si1074829ywg.1.2016.09.12.04.02.25
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 12 Sep 2016 04:02:25 -0700 (PDT)
Received-SPF: neutral (google.com: 2607:f8b0:400d:c09::229 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c09::229;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com;
       spf=neutral (google.com: 2607:f8b0:400d:c09::229 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Received: by mail-qk0-x229.google.com with SMTP id w204so137656838qka.0
        for <HomotopyT...@googlegroups.com>; Mon, 12 Sep 2016 04:02:25 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=andrej-com.20150623.gappssmtp.com; s=20150623;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to;
        bh=e8+j11eLr3LHOifyrAfSm/o8k/R0KI095KJ/FFrhmGA=;
        b=1KqRHmIAFZlCMrGubTZ8D2O3yGZ4/eLRdgefTLcWFHgrZ4xb67wmis9GRtvBUN7x8l
         Puxelykt2cwrty+4CoTgxzYuOYCgBifz2LGeM7pWMmlOloqtdnia/9R3m8XGH95sdTO5
         ymXzsD3odQDT931AWstgv3a1SoRCut7g8gkcmzPPks4sZVnl/nd1jxbBWtYnoKk2la/W
         i8+jkFYSaczvw4dStjDxXB6HTaWZaX7e39HrzDP9kEB1FKJiyyo6WpH4S8O7W6EvzCTD
         5DZoUGZA396En0dEeZctjubeHwmTzEMu4Ouj9RUNcpbUPB9jlu3GLbhstDLhJWXA9+xI
         p3GQ==
X-Gm-Message-State: AE9vXwO285HMP4c85l0Ws5d1LVGJPt8ex0ntgRFe6o8Wn4Ve6iOP34RJhUQ0LDNM4Yfg1Ht4FpoRV4xavfilWQ==
X-Received: by 10.55.178.69 with SMTP id b66mr18308254qkf.146.1473678145426;
 Mon, 12 Sep 2016 04:02:25 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.55.53.70 with HTTP; Mon, 12 Sep 2016 04:02:24 -0700 (PDT)
In-Reply-To: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com>
References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com>
From: Andrej Bauer <andrej...@andrej.com>
Date: Mon, 12 Sep 2016 13:02:24 +0200
Message-ID: <CAB0nkh2eZT+yOVDmdxPdkg2iKuvJFU2W=Qd_MmM1=CW9tFrDNw@mail.gmail.com>
Subject: Re: [HoTT] Meta-conjecture about MLTT
To: Martin Escardo <escardo...@googlemail.com>, 
	"HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8

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