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
10 of 11 tasks
fredrik-bakke opened this issue Mar 30, 2024 · 0 comments
Open
10 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
Loading

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.
@fredrik-bakke fredrik-bakke mentioned this issue Aug 2, 2024
Merged
VojtechStep pushed a commit that referenced this issue Aug 21, 2024
@fredrik-bakke
Literature – Idempotents in Intensional Type Theory (#1160)
da7a12c 
Adds a literature file for the article _Idempotents in Intensional Type
Theory_ by Shulman. Most of sections 1-3, 5, and 9 are formalized.

#1103 #1055
morphismz pushed a commit to morphismz/agda-unimath that referenced this issue Sep 10, 2024
@fredrik-bakke @morphismz
Literature – Idempotents in Intensional Type Theory (UniMath#1160)
3772e89 
Adds a literature file for the article _Idempotents in Intensional Type
Theory_ by Shulman. Most of sections 1-3, 5, and 9 are formalized.

UniMath#1103 UniMath#1055
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