Splitting idempotents - Githubissues

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

219 stars 70 forks source link

Splitting idempotents #1105

Closed fredrik-bakke closed 5 months ago

fredrik-bakke commented 6 months ago

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 commented 6 months ago

Since I won't be able to finish this PR before I leave tomorrow, let me write down some thoughts here for when I pick this up again.

It remains to show that is-split-idempotent-map f is a retract of is-quasiidempotent-map f
The splitting of this retract gives us an infinitely coherent definition of idempotent maps.

It's sensible to make a new file for infinitely coherent idempotent maps, but then one may ask if the proof that quasiidempotents split fits better in that file. There is also a question of whether we want more agda-unimath like names for is-preidempotent and is-quasiidempontent. My initial suggestions would be is-idempotent for the former, mirroring e.g. is-involution which is not coherent either, and is-quasicoherent-idempotent for the latter.

I should also write informal proofs for the main results, and this shouldn't be difficult.
Remark on the explicit counter-examples given in the paper.

Any other nice and easy consequences of this formalization?

fredrik-bakke commented 6 months ago

I also need to verify that the diagrams render properly

fredrik-bakke commented 6 months ago

To partition this work up a bit, I may aim to formalize fully coherent idempotents in a subsequent PR. It still remains to tidy up this PR before it is ready for review, however.

fredrik-bakke commented 5 months ago

A couple of questions remain:

where should is-small-retract be placed? It cannot be placed in either retracts-of-types or small-types due to cyclic dependency issues.
am I right to change the terminology of "preidempotent map" to "idempotent map", "quasiidempotent map" to "quasicoherently idempotent map", and "idempotent map" to "coherently idempotent map"?
What are the best names for right-right-inv and its cousins?

fredrik-bakke commented 5 months ago

This PR is now open to reviews. @tomdjong said he was interested in reviewing this, so I'll tag him :)

fredrik-bakke commented 5 months ago

Is this PR ready to merge? I can formalize the counter-example in a subsequent PR thanks to #1115

EgbertRijke commented 5 months ago

Is this PR ready to merge? I can formalize the counter-example in a subsequent PR thanks to #1115

Great work, I'll turn on the auto-merge