Skip to content

Improve presentation of funext and univalence metatheory #563

Open
mikeshulman opened this Issue Dec 1, 2013 · 1 comment

2 participants

@mikeshulman

I propose that in the second edition, we improve the presentation of metatheoretic facts about funext and univalence. I think we originally tried to minimize metatheoretic discussion out of an attempt to keep the book focused on one theory, but issues and questions that have arisen since then suggest that some additional minimal amount of metatheory needs to be included. We've stuck them in exercises for the first edition, but it might be better to concentrate them.

Here's a concrete proposal: at the end of chapter 4, in addition to the current (metatheoretic) section 4.9 (univalence implies funext), we include a section proving "weak funext implies strong funext" (currently exercise 2.16 and theorem 4.9.5) and a section proving the inconsistency of qinv-univalence (currently exercise 4.6). The former is essentially already used in 4.9, but as was pointed out recently, it is also needed in section 6.3; while the latter is important (remark 2.10.4) to justify all the work that goes into defining a good "isequiv" in chapter 4.

@RobertHarper
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.