Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Idempotents in Intensional Type Theory #1103

Open
8 of 11 tasks
fredrik-bakke opened this issue Mar 30, 2024 · 0 comments
Open
8 of 11 tasks

Idempotents in Intensional Type Theory #1103

fredrik-bakke opened this issue Mar 30, 2024 · 0 comments
Assignees
@fredrik-bakke
Labels
formalization-target foundation

Comments

@fredrik-bakke
Copy link
Collaborator

fredrik-bakke commented Mar 30, 2024 •
edited

Goals

Overarching goal: formalize the positive results from Idempotents in Intensional Type Theory.

  • Infrastructure for the total type of retracts of a type
  • Infrastructure for sequential limits Sequential limits #839
  • The splitting type of a split idempotent map is essentially unique
  • Split idempotents are quasiidempotent
  • Preidempotents on sets split
  • Weakly constant preidempotents split
  • Quasiidempotents split
  • Split idempotents are a retract of quasiidempotents
  • The type of (fully coherent) idempotents as the splitting type of the above retract
  • Write paper summary file
  • Include explanations regarding the negative results, although this issue does not aim to have them formalized.

References

  • Michael Shulman, Idempotents in Intensional Type Theory, arXiv:1507.03634
  • Michael Shulman, Splitting Idempotents, HoTT blog post
  • Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch, Notions of Anonymous Existence in Martin-Löf Type Theory, arXiv:1610.03346
@fredrik-bakke fredrik-bakke self-assigned this Mar 30, 2024
@fredrik-bakke fredrik-bakke mentioned this issue Mar 30, 2024
Merged
EgbertRijke pushed a commit that referenced this issue Apr 17, 2024
@fredrik-bakke
Splitting idempotents (#1105)
f4400b1 
### Summary
- Retracts of a type
  - Define retracts of a type 
  - Characterize equality of retracts
- Weakly constant maps
  - The type of fixed points of weakly constant maps is a proposition
- Idempotent maps
- Rename "preidempotent maps" to "idempotent maps". This mirrors how we
treat "invertible maps" vs "coherently invertible maps", although there
is an essential difference between the two concepts: idempotent maps are
not "coherentifiable" like invertible maps. That role is taken by
"quasicoherently idempotent maps" instead.
- Quasicoherently idempotent maps (called "quasiidempotent maps" in
[Shu17])
  - Define quasicoherently idempotent maps
- Quasicoherently idempotent maps are closed under homotopy (without
funext)
- Split idempotent maps
  - Define split idempotent maps
  - Split idempotent maps are quasicoherently idempotent
  - Idempotent maps on sets split
  - Weakly constant idempotent maps split
  - Quasicoherently idempotent maps split
- Retracts of small types are small

Work towards #1103.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@fredrik-bakke fredrik-bakke

Labels
formalization-target foundation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@fredrik-bakke