From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 7 Mar 2018 19:50:46 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> Subject: Re: Univalence from scratch MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_859_92627402.1520481046844" ------=_Part_859_92627402.1520481046844 Content-Type: multipart/alternative; boundary="----=_Part_860_933540442.1520481046845" ------=_Part_860_933540442.1520481046845 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable The paper of Martin-L=C3=B6f that you cite is about extensional type theory= , not=20 intensional type theory. In particular, in that paper, it's not the case=20 that "Types are constructed together with their elements, and not by=20 collecting some previously existing elements." as you write. You should=20 probably cite something else. (Otherwise, looks good to me!) I think the system you want was introduced in "An Intuitionistic Theory of= =20 Types: Predicative Part" (1975)=20 (http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-T= ypes-Predicative-Part-1975.pdf).=20 But it doesn't have a nice concise description of the formal system. On Wednesday, March 7, 2018 at 4:10:54 PM UTC-5, Mart=C3=ADn H=C3=B6tzel Es= card=C3=B3=20 wrote: > > I have often seen competent mathematicians and logicians, outside our=20 > circle, making technically erroneous comments about the univalence axiom,= =20 > in conversations, in talks, and even in public material, in journals or t= he=20 > web.=20 > > For some time I was a bit upset about this. But maybe this is our fault,= =20 > by often trying to explain univalence only imprecisely, mixing the=20 > explanation of the models with the explanation of the underlying theory= =20 > (MLTT, identity types, universe), with none of the two explained=20 > sufficiently precisely.=20 > > There are long, precise explanations such as the HoTT book, for example,= =20 > or, the formalizations in Coq, Agda and Lean. > > But perhaps we don't have publicly available material with a=20 > self-contained, brief and complete formulation of univalence, so that=20 > interested mathematicians and logicians can try to contemplate the axiom = in=20 > a fully defined form. > > Here is an attempt to rectify this: > > https://arxiv.org/abs/1803.02294 > > This also has an ancillary Agda file with univalence defined from scratch= =20 > (without the use of any library at all). Perhaps somebody should add a Co= q=20 > "version from scratch" of this.=20 > > There is also a web version of this ( > http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html) to try= =20 > to make this as accessible as possible, with the text and the Agda code= =20 > together. > > M. > > ------=_Part_860_933540442.1520481046845 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
The paper of Martin-L=C3=B6f that you cite is about extens= ional type theory, not intensional type theory. In particular, in that pape= r, it's not the case that "Types are constructed together with the= ir elements, and not by collecting some previously existing elements."= as you write. You should probably cite something else. (Otherwise, looks g= ood to me!)

I think the system you want was introduced in "An I= ntuitionistic Theory of Types: Predicative Part" (1975) (http://archiv= e-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-Predicati= ve-Part-1975.pdf). But it doesn't have a nice concise description of th= e formal system.

On Wednesday, March 7, 2018 at 4:10:54 PM UTC-5, Ma= rt=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote:
I have often seen competent mathematicians and = logicians, outside our circle, making technically erroneous comments about = the univalence axiom, in conversations, in talks, and even in public materi= al, in journals or the web.=C2=A0

For some time I was a = bit upset about this. But maybe this is our fault, by often trying to expla= in univalence only imprecisely, mixing the explanation of the models with t= he explanation of the underlying theory (MLTT, identity types, universe), w= ith none of the two explained sufficiently precisely.=C2=A0

<= /div>
There are long, precise explanations such as the HoTT book, for e= xample, or, the formalizations in Coq, Agda and Lean.

<= div>But perhaps we don't have publicly available material with a self-c= ontained, brief and complete formulation of univalence, so that interested = mathematicians and logicians can try to contemplate the axiom in a fully de= fined form.

Here is an attempt to rectify this:

This also has an ancillary Agda file wi= th univalence defined from scratch (without the use of any library at all).= Perhaps somebody should add a Coq "version from scratch" of this= .=C2=A0

There is also a web version of this (http://www.cs.bham.ac.uk/~mhe/agd= a-new/UnivalenceFromScratch.html) to try to make this as accessibl= e as possible, with the text and the Agda code together.

M.

------=_Part_860_933540442.1520481046845-- ------=_Part_859_92627402.1520481046844--