From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Wed, 7 Jun 2017 23:35:24 -0700 (PDT)
From: Andrew Swan <wakeli...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Cc: wakeli...@gmail.com, awo...@cmu.edu, Thierry...@cse.gu.se
Message-Id: <9c8e516a-a09b-4632-8cd1-ccf7a0211cfd@googlegroups.com>
In-Reply-To: <CAOvivQwJ_Dd=HCVmsYL2sPtHCv4USrwHTBzP6E50aX-iuruoFg@mail.gmail.com>
References: <CAOvivQwZFp_uopf53SGstTgbojnQ67i-bR70j5q8E5JTUGubDg@mail.gmail.com>
 <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu>
 <CAOvivQySuTrKMj4n_nP+6BqrnBSQ+=zYhVVL1p4Rx8GYHQmvrA@mail.gmail.com>
 <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> <CAAkwb-nogDyVRwnvDXUphBQb0ttL-TuHfSahnrSMhFnuunc7hw@mail.gmail.com>
 <CAAkwb-k1GnZKkrEoszNQQ0zyA3HSFh1LXmKVp-+3juRk5s8taQ@mail.gmail.com> <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com>
 <CAOvivQwJ_Dd=HCVmsYL2sPtHCv4USrwHTBzP6E50aX-iuruoFg@mail.gmail.com>
Subject: Re: [HoTT] Semantics of higher inductive types
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_215_367460613.1496903724412"

------=_Part_215_367460613.1496903724412
Content-Type: multipart/alternative; 
	boundary="----=_Part_216_1579665615.1496903724412"

------=_Part_216_1579665615.1496903724412
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit


>
> Why is there no LOG in this? 


It's a little messy to write out the actual details, but it is possible for 
each map f : X -> Y to use the subobject classifier and dependent products 
to construct a "universal lifting problem" for f, where universal means 
that every other lifting problem against a pushout product of monomorphism 
and i-endpoint inclusion factors uniquely as a pullback followed by the 
universal lifting problem. Then, once a filler for the universal lifting 
problem has been chosen, it can be used to construct a filler for all the 
other lifting problems. (This can also be seen as an instance of a general 
result that holds in any locally small fibration with finitely complete 
base).

------=_Part_216_1579665615.1496903724412
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><blockquote class=3D"gmail_quote" style=3D"margin: 0px 0px=
 0px 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">=
Why is there no LOG in this?=C2=A0</blockquote><div><br></div><div>It&#39;s=
 a little messy to write out the actual details, but it is possible for eac=
h map f : X -&gt; Y to use the subobject classifier and dependent products =
to construct a &quot;universal lifting problem&quot; for f, where universal=
 means that every other lifting problem against a pushout product of monomo=
rphism and i-endpoint inclusion factors uniquely as a pullback followed by =
the universal lifting problem. Then, once a filler for the universal liftin=
g problem has been chosen, it can be used to construct a filler for all the=
 other lifting problems. (This can also be seen as an instance of a general=
 result that holds in any locally small fibration with finitely complete ba=
se).</div></div>
------=_Part_216_1579665615.1496903724412--

------=_Part_215_367460613.1496903724412--