Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Jon Sterling <jon@jonmsterling.com>
To: Urs Schreiber <urs.schreiber@googlemail.com>
Cc: Egbert Rijke <e.m.rijke@gmail.com>,
	Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv
Date: Tue, 03 Jan 2023 23:05:54 +0100	[thread overview]
Message-ID: <B7706C57-2DE8-4AB6-A50B-89F7E6C1067D@jonmsterling.com> (raw)
In-Reply-To: <CA+KbugeyU16TCLH9MbiBPUQHFiqytnpftQ=FmPr8zLSzk1ODHA@mail.gmail.com>

Hi all,

I second Urs's congratulations on this great achievement! Just want to also add that I likewise miss the material on descent & flattening, for which your old notes provided an excellent reference. Of course, perhaps this leaves room for an "Advanced Topics in Homotopy Type Theory" followup ;-)

Best,
Jon


On 3 Jan 2023, at 20:16, 'Urs Schreiber' via Homotopy Type Theory wrote:

> Hi Egbert,
>
> nice to see your notes now available in a stably referenceable way!
> They could fill quite a few gaps that the existing textbook literature
> leaves open.
>
> On that note, it seems that a fair bit of material has been removed in
> the arXiv version?
> (Maybe to make room for large margins?)
>
> For referencing on the nLab I now find myself pointing mainly to the
> version of your notes from 2018 (these here:
> https://www.andrew.cmu.edu/user/erijke/hott/hott_intro.pdf), which
> have discussion for instance of homotopy pullbacks/pushouts that seem
> to have later been dropped, together with much material depending on
> these notions (if I am seeing this correctly ?)
>
> I can imagine this is at least in large part the publisher's decision,
> but just to say that if there is any wiggle room left, then I would
> think it most worthwhile if these topics could make it into the final
> book version.
>
> All my best wishes for the New Year,
> Urs
>
> On Fri, Dec 23, 2022 at 1:54 PM Egbert Rijke <e.m.rijke@gmail.com> wrote:
>>
>> Dear homotopy type theorists,
>>
>> My textbook Introduction to Homotopy Type Theory is finished and available on the ArXiv:
>>
>> https://arxiv.org/abs/2212.11082
>>
>> From the abstract:
>> This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-Löf's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.
>>
>> Over Christmas I will write a blog post in which I will go more into the content of the book. For now: Enjoy!
>>
>> Happy holidays to everyone!
>> Egbert
>>
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChxg%40mail.gmail.com.
>
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BKbugeyU16TCLH9MbiBPUQHFiqytnpftQ%3DFmPr8zLSzk1ODHA%40mail.gmail.com.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/B7706C57-2DE8-4AB6-A50B-89F7E6C1067D%40jonmsterling.com.

  reply	other threads:[~2023-01-03 22:06 UTC|newest]

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-12-23  9:54 Egbert Rijke
2022-12-23 14:22 ` João Alves Silva Júnior
2022-12-23 22:51 ` 'EMILY RIEHL' via Homotopy Type Theory
2023-01-03 19:16 ` 'Urs Schreiber' via Homotopy Type Theory
2023-01-03 22:05   ` Jon Sterling [this message]
2023-01-13 14:52     ` Madeleine Birchfield

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=B7706C57-2DE8-4AB6-A50B-89F7E6C1067D@jonmsterling.com \
    --to=jon@jonmsterling.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=e.m.rijke@gmail.com \
    --cc=urs.schreiber@googlemail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).