From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.46.1.27 with SMTP id 27mr769559ljb.10.1473328269585;
        Thu, 08 Sep 2016 02:51:09 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.71.16 with SMTP id u16ls694270wma.12.gmail; Thu, 08 Sep
 2016 02:51:08 -0700 (PDT)
X-Received: by 10.28.193.198 with SMTP id r189mr1374297wmf.7.1473328268878;
        Thu, 08 Sep 2016 02:51:08 -0700 (PDT)
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx500.hrz.tu-darmstadt.de (mail-relay14.hrz.tu-darmstadt.de. [130.83.156.238])
        by gmr-mx.google.com with ESMTPS id w134si635412wmf.3.2016.09.08.02.51.08
        for <HomotopyT...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Thu, 08 Sep 2016 02:51:08 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.238 as permitted sender) client-ip=130.83.156.238;
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.238 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 lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id u889p727010384;
	Thu, 8 Sep 2016 11:51:08 +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 u889p770014969;
	Thu, 8 Sep 2016 11:51:07 +0200
Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003)
	id CC7651A3C0F; Thu,  8 Sep 2016 11:51:07 +0200 (CEST)
Date: Thu, 8 Sep 2016 11:51:07 +0200
From: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
To: Martin Escardo <escardo...@googlemail.com>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] A puzzle about "univalent equality"
Message-ID: <20160908095107.GA25319@mathematik.tu-darmstadt.de>
References: <CABcT7WBZo8bt6dtfDowd2nOYrtLPwsCC4Yxara1sZ5_oHeUQFw@mail.gmail.com>
 <CAOvivQwgfVzH9N_JhgdjB4KC5+LmMEjAJpO-mKo_Mm70OOgr4w@mail.gmail.com>
 <CAAkwb-mYObk7m+FwBosiPcbm9p7mo2z5Lw-3LUtg4Di2X-pYxg@mail.gmail.com>
 <CABcT7WDg9P8GcAfihWz4mF-upkzzo1sjneax2nKedutMHUpzzg@mail.gmail.com>
 <143ade6b-1b68-36fe-a765-c54d9f6fac8c@googlemail.com>
 <a88b7834-5ce8-47d6-803a-d2a98ed27084@googlegroups.com>
 <CAOvivQxFDPaVL0iwDR=sBMWa+Zmh56jatW24-Bv7n0ar4FvaSA@mail.gmail.com>
 <d53d7569-5d1f-429d-8b83-1e8c1628d8a2@googlegroups.com>
 <CAOvivQxCQ3XGbBn0sQ9wrrPs7hsWD3FkkW1SO1t-PrJCfmq01w@mail.gmail.com>
 <e40b8630-9d14-53c7-b94a-0441e4776b2c@googlemail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <e40b8630-9d14-53c7-b94a-0441e4776b2c@googlemail.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.8.94218
X-PMX-RELAY: outgoing

Intensional type theory is consistent with extensional type theory
which can be interpreted in any  locally cartesian category. Equality
is there interpreted via diagonals (in slice categories). This does
not at all assume quantification over an untyped universe.

Adding K to ITT is an attempt to approach ETT and keeping type
checking decidable.

Most of the known models of type theory are models of extensional type
theory. This collection contains all lcc's and all toposes. I have no
problem to recall these...

Models of ITT but not of ETT and not validating Univalence were
constructed in my Habilitation Thesis and more recently in the Thesis
of Tamara von Glehn.

Thomas