Generalizations of Hedberg's Theorem and Kraus' Lemma #333
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mortberg
requested changes
Jun 8, 2020
|
It is better to use "split support" (apparently this terminology comes from (1-)topos theory, according to Mike Shulman) rather than hstable. The published version is in LMCS. https://lmcs.episciences.org/3217. The first proof that the type of fixed points of a weakly constant endomap is a proposition is due to Nicolai Kraus. Then other people, including Sattler, came up with simpler proofs (I think Sattler's proof is mentioned in our LMCS paper). I also have a simplified proof here: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#fix-is-subsingleton |
|
This looks good to me now! I'd be happy to merge as soon as Travis is done. Thanks for the contribution! |
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Introduces fixpoints, Kraus's Lemma and nullary relations found in "Generalizations of Hedberg's Theorem". We get the implications:
The proof of Kraus' lemma in particular is short compared to the version found in the originally associated agda code
A bit of bikeshedding over naming is expected, for example
SplitSupportis currently aliased toHStable, etc. Suffix -≡ is supposed to mean "on all path spaces", as originally used inDecidableEq, but I personally find myself skipping over the suffix in some situations when reading the code.