Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series

["'Urs Schreiber' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.com>]

On Thu, Apr 14, 2022 at 5:28 AM Chris Kapulkin <k.kapulkin@gmail.com> wrote:

> We believe the speaker’s recent statements in the context of the HoTT
> Book stand in opposition to these values

Scrolling up this thread for context, one gathers you must be
referring to this statement:

 "In Book HoTT, identity is defined uniformly [...] many desired
equalities are not definitional".

While possibly scandalous, I am tolerant and was looking forward to
seeing the arguments,
if not for moral but for intellectual edification.

Is there a draft or preprint available of the announced work by
Altenkirch, Shulman & Kaposi?
It sounds intriguing.

-- 
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%2BKbugem61xD06bxhHvd5vuUJdHrt%2BCJu0%2BYoJvNBM57jCxJCA%40mail.gmail.com.