From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.93.20 with SMTP id r20mr1009215wmb.5.1466099482787; Thu, 16 Jun 2016 10:51:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.197.142 with SMTP id v136ls136666wmf.53.gmail; Thu, 16 Jun 2016 10:51:22 -0700 (PDT) X-Received: by 10.28.154.151 with SMTP id c145mr1008768wme.3.1466099482211; Thu, 16 Jun 2016 10:51:22 -0700 (PDT) Return-Path: Received: from mail-lf0-x231.google.com (mail-lf0-x231.google.com. [2a00:1450:4010:c07::231]) by gmr-mx.google.com with ESMTPS id y8si1048882lbi.2.2016.06.16.10.51.22 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 10:51:22 -0700 (PDT) Received-SPF: pass (google.com: domain of ericf...@gmail.com designates 2a00:1450:4010:c07::231 as permitted sender) client-ip=2a00:1450:4010:c07::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of ericf...@gmail.com designates 2a00:1450:4010:c07::231 as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x231.google.com with SMTP id j7so45421906lfg.1 for ; Thu, 16 Jun 2016 10:51:22 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=i7JAvu+kVPVzDjjmFgj8c+q0aCHa/0DAwFzXdKs37oA=; b=vEfT58h8OcKLVm9JIxH/lXPwu9BcDgkcq5h6/4FltZRagX99nEs2wmkPh6ryu+Zvqh qJiGag7LvuOiuUbvM/QfAqYindl/DigdZGrNiAoMm6gj7dT+lG7Q1+evP/XXY3uS0bPY +Of6vkhRJ5UIPoee7jPBIB28YPKcF8MdBkJcjdhB1QfdDZblCKX/T+U8JKIicTk632zg 1xQCnYCaFE7gSOJJyagLlGdcpkzztvmN8g+AmhERGsE6GdUCUdPJdJxg2Efj8HgJAFdA +9KUEn2GtOxSDtH+ypWQdIouNfqTT8UMKIqhXeIP7WPTke4P36C4WQ4sSDuw6P+LBiQP EnkQ== X-Gm-Message-State: ALyK8tKLdToxHguQycgXELHkqkz2O47+UyXo0HB0EjRndaoV/MvIUK8OcOBTDeVnAOHkOi0IHHlCuCO4xn4EbQ== X-Received: by 10.25.22.70 with SMTP id m67mr1362655lfi.25.1466099481967; Thu, 16 Jun 2016 10:51:21 -0700 (PDT) MIME-Version: 1.0 References: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> <932D947A-BCD6-4B7A-BBB6-86077A70F414@chalmers.se> In-Reply-To: <932D947A-BCD6-4B7A-BBB6-86077A70F414@chalmers.se> From: Eric Finster Date: Thu, 16 Jun 2016 17:51:12 +0000 Message-ID: Subject: Re: [HoTT] Is synthetic the right word? To: Thierry Coquand Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a11406e54d40485053568e207 --001a11406e54d40485053568e207 Content-Type: text/plain; charset=UTF-8 Hi Thierry, > A small remark about this: at least we can interpret type theory with the > univalence > axiom in the (iterated) presheaf category > > [Fin_*, [C^op, Set]] > > where C is the category of cubes we have considered for cubical type theory > (since we know how to interpret universes in presheaf categories and all > the operations > relativize to presheafs; on the other hand, it is not clear yet how to > relativize it for -sheaf- models > since it is less clear how universes should be interpreted). > We also should have a purely syntactical version, where judgements are > indexed not only over a finite set > but over a pair of a finite set and a pointed finite set. > > Very interesting remark. I'm not quite sure this quite corresponds to what I had in mind, since I was thinking of the infty-category of presheaves on the infty-category of finite pointed spaces. (That is, by Fin_* I mean finite *spaces*, not finite sets... sorry if my notation was bad) With this in mind, I guess in the remark this would correspond to something like considering the "enriched" presheaves with some chosen model structure. But I'm getting a bit out of my depth here so maybe someone can chime in to help me out ... So it looks to me like you are saying something like that the cubical model should tell us how to interpret type theory in an infinity-topos of presheaves on an arbitrary 1-category? Is this right, or am I misunderstanding? Or was Fin_* special for some reason (though, again, Fin_* for me was finite spaces, not finite sets ...)? Can I replace Fin_* with D for any category D? Fin_* certainly falls outside of the EI-category restriction, and I was not aware that we knew how to lift that. Does cubical type theory give a way or have I completely missed the point? :p Cheers, Eric --001a11406e54d40485053568e207 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hi Thierry,
=C2=A0
=C2=A0A small remark about t= his: at least we can interpret type theory with the univalence=C2=A0
axiom in the (iterated) presheaf category

=C2=A0[Fin_*, [C^op, Set]]

where C is the category of cubes we have considered for cubical type t= heory
(since we know how to interpret universes in presheaf categories and a= ll the operations
relativize to presheafs; on the other hand, it is not clear yet how to= relativize it for -sheaf- models
since it is less clear how universes should be interpreted).
We also should have a purely syntactical version, where judgements are= indexed not only over a finite set
but over a pair of a finite set and a pointed finite set.
<= div style=3D"word-wrap:break-word">


Very interesting rema= rk.

I'm not quite sure this quite corresponds to w= hat I had in mind, since I was thinking of the=C2=A0
infty-category of presheaves on the infty-catego= ry of finite pointed spaces. =C2=A0(That is,
by Fin_* I mean finite *spaces*, not finite sets... so= rry if my notation was bad) =C2=A0With this in mind, I guess=C2=A0
in the remark this would correspon= d to something like considering the "enriched"=C2=A0
=
presheaves with some chosen model stru= cture.=C2=A0 But I'm getting a bit out of my depth here
so maybe someone can chime in to help me = out ...

<= div>So it looks to me like you are saying s= omething like that the cubical model should tell
us how to interpret type theory in an infinity-topos= of presheaves on an arbitrary 1-category?
Is this right, or am I misunderstanding?=C2=A0Or was Fin_* special for some reason (though,=C2= =A0
again, Fin_* for me wa= s finite spaces, not=C2=A0finite set= s ...)?=C2=A0 Can I replace Fin_* with D for any category D?

Fin_* certainly falls outside of the EI-category restriction,= and I was not aware that
we knew how to lift that.=C2=A0 = Does cubical type theory give a way or have I completely missed the point? = =C2=A0:p

Cheers,

Eric
--001a11406e54d40485053568e207--