On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <
awo...@cmu.edu> wrote:
>
> yo=
u mean the propositional truncation or suspension operations might lead to =
cardinals outside of a Grothendieck Universe?
Exactly, yes.=C2=A0 Th=
ere=E2=80=99s no reason I know of to think they *need* to, but with the con=
struction of Mike=E2=80=99s and my paper, they do.=C2=A0 And adding stronge=
r conditions on the cardinal used won=E2=80=99t help.=C2=A0 The problem is =
that one takes a fibrant replacement to go from the =E2=80=9Cpre-suspension=
=E2=80=9D to the suspension (more precisely: a (TC,F) factorisation, to go =
from the universal family of pre-suspensions to the universal family of sus=
pensions); and fibrant replacement blows up the fibers to be the size of th=
e *base* of the family.=C2=A0 So the pre-suspension is small, but the suspe=
nsion =E2=80=94 although essentially small =E2=80=94 ends up as large as th=
e universe one=E2=80=99s using.
So here=E2=80=99s a very precise pro=
blem which is as far as I know open:
(*) Construct an operation =CE=
=A3 : U =E2=80=93> U, where U is Voevodsky=E2=80=99s universe, together =
with appropriate maps N, S : =C3=9B =E2=80=93> =C3=9B over =CE=A3, and a=
homotopy m from N to S over =CE=A3, which together exhibit U as =E2=80=9Cc=
losed under suspension=E2=80=9D.
I asked a related question on matho=
verflow a couple of years ago:
https://mathoverflow.net/questions/219588/pullback-stable-mod=
el-of-fibrewise-suspension-of-fibrations-in-simplicial-sets =C2=A0David=
White suggested he could see an answer to that question (which would proba=
bly also answer (*) here) based on the comments by Karol Szumi=C5=82o and T=
yler Lawson, using the adjunction with Top, but I wasn=E2=80=99t quite able=
to piece it together.
=E2=80=93p.
=C2=A0
>
> > On=
Jun 1, 2017, at 11:38 AM, Michael Shulman <
shu...@sandiego.edu> wrote:
> >
> > Do =
we actually know that the Kan simplicial set model has a *universe
> =
> closed under* even simple HITs?=C2=A0 It's not trivial because thi=
s would
> > mean we could (say) propositionally truncate or suspen=
d the generic
> > small Kan fibration and get another *small* Kan =
fibration, whereas the
> > base of these fibrations is not small, =
and fibrant replacement doesn't
> > in general preserve smalln=
ess of fibrations with large base spaces.
> >
> > (Also, =
the current L-S paper doesn't quite give a general syntactic
> &g=
t; scheme, only a general semantic framework with suggestive implications
> > for the corresponding syntax.)
> >
> >
>=
; >
> > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey <awo...@cmu.edu> wrote:
> >><=
br>> >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thierry...@cse.gu.se>
> >&=
gt; wrote:
> >>
> >> =C2=A0If we are only intereste=
d in providing one -particular- model of HITs,
> >> the paper> >> on =C2=A0cubical type =C2=A0theory describes a way to =C2=
=A0interpret HIT together with a
> >> univalent
> >>=
; universe which is stable by HIT operations. This gives in particular the<=
br>> >> consistency
> >> and the proof theoretic power=
of this extension of type theory.
> >>
> >>
>=
; >> but the Kan simplicial set model already does this =E2=80=94 rig=
ht?
> >> don=E2=80=99t get me wrong =E2=80=94 I love the cubes,=
and they have lots of nice properties
> >> for models of HoTT<=
br>> >> =E2=80=94 but there was never really a question of the con=
sistency or coherence of
> >> simple HITs like propositional tr=
uncation or suspension.
> >>
> >> the advance in th=
e L-S paper is to give a general scheme for defining HITs
> >> =
syntactically
> >> (a definition, if you like, of what a HIT is=
, rather than a family of
> >> examples),
> >> and =
then a general description of the semantics of these,
> >> in a=
range of models of the basic theory.
> >>
> >> Ste=
ve
> >>
> >>
> >> =C2=A0The approach us=
es an operation of =C2=A0=E2=80=9Cflattening an open box=E2=80=9D, which so=
lves
> >> in
> >> this case the issue of interpreti=
ng HIT with parameters (such as
> >> propositional
> >=
> truncation or suspension) without any coherence issue.
> >>=
; Since the syntax used in this paper is so close to the semantics, =C2=A0w=
e
> >> limited
> >> ourselves =C2=A0to a syntactica=
l presentation of this interpretation. But it can
> >> directly=
> >> be transformed to a semantical interpretation, as explain=
ed in the following
> >> note
> >> (which also inco=
rporates a nice simplification of the operation of
> >> flatter=
ing
> >> an open box noticed by my coauthors). I also try to ma=
ke more explicit in
> >> the note
> >> what is the =
problem solved by the =E2=80=9Cflattening boxes=E2=80=9D method.
> &g=
t;>
> >> Only the cases of the spheres and propositional tru=
ncation are described,
> >> but one
> >> would expe=
ct the method to generalise to other HITs covered e.g. in the HoTT
> =
>> book.
> >>
> >> On 25 May 2017, at 20:25, =
Michael Shulman <shu...@sandiego.=
edu> wrote:
> >>
> >> The following long-awa=
ited paper is now available:
> >>
> >> Semantics of=
higher inductive types
> >> Peter LeFanu Lumsdaine, Mike Shulm=
an
> >> https://ar=
xiv.org/abs/1705.07088
> >>
> >> From the abstr=
act:
> >>
> >> We introduce the notion of *cell mon=
ad with parameters*: a
> >> semantically-defined scheme for spe=
cifying homotopically well-behaved
> >> notions of structure. W=
e then show that any suitable model category
> >> has *weakly s=
table typal initial algebras* for any cell monad with
> >> para=
meters. When combined with the local universes construction to
> >=
> obtain strict stability, this specializes to give models of specific> >> higher inductive types, including spheres, the torus, pusho=
ut types,
> >> truncations, the James construction, and general=
localisations.
> >>
> >> Our results apply in any =
sufficiently nice Quillen model category,
> >> including any ri=
ght proper simplicial Cisinski model category (such as
> >> sim=
plicial sets) and any locally presentable locally cartesian closed
> =
>> category (such as sets) with its trivial model structure. In
&g=
t; >> particular, any locally presentable locally cartesian closed
> >> (=E2=88=9E,1)-category is presented by some model category t=
o which our
> >> results apply.
> >>
> >&g=
t; --
> >> You received this message because you are subscribed=
to the Google Groups
> >> "Homotopy Type Theory" gro=
up.
> >> To unsubscribe from this group and stop receiving emai=
ls from it, send an
> >> email to HomotopyTypeThe...@googlegroups.com.
>=
>> For more options, visit https://groups.google.com/d/optout.
> >>
> >=
>
> >>
> >> --
> >> You received thi=
s message because you are subscribed to the Google Groups
> >> =
"Homotopy Type Theory" group.
> >> To unsubscribe fro=
m this group and stop receiving emails from it, send an
> >> em=
ail to HomotopyType=
The...@googlegroups.com.
> >> For more options, visit https://groups.google.com/d/optou=
t.
> >>
> >>
> >> --
> >&g=
t; You received this message because you are subscribed to the Google Group=
s
> >> "Homotopy Type Theory" group.
> >>=
To unsubscribe from this group and stop receiving emails from it, send an<=
br>> >> email to HomotopyTypeThe...@googlegroups.com.
> >> For more o=
ptions, visit https://groups=
.google.com/d/optout.
> >
> > --
> > You rec=
eived this message because you are subscribed to the Google Groups "Ho=
motopy Type Theory" group.
> > To unsubscribe from this group=
and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.<=
br>> > For more options, visit https://groups.google.com/d/optout.
>
> --
>=
You received this message because you are subscribed to the Google Groups =
"Homotopy Type Theory" group.
> To unsubscribe from this gr=
oup and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
--94eb2c0433460e72ba0550e841da--