Splitting idempotents

[fredrik-bakke]

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]

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]

I also need to verify that the diagrams render properly

[fredrik-bakke]

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.

[EgbertRijke]

This is a very nice pull request, with many excellent new additions. Thank you so much for making this effort Fredrik!

[tomdjong]

Very nice to see this formalized, @fredrik-bakke!

[fredrik-bakke]

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

[EgbertRijke]

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