Basic properties of the flat modality

[fredrik-bakke]

This is the replacement of #1005.

Proves a series of basic properties of the flat modality.

Summary

General properties

• [X] The universal property of flat discrete crisp types
• [x] ~The dependent universal property of flat discrete crisp types~
• [X] Functoriality of flat
• [X] Flat is idempotent
• [x] A crisp type is crisply flat discrete if its counit has a crisp section

Left exactness of flat

• [X] Flat distributes over identity types
• [X] The crisp identity types of flat discrete crisp types are flat discrete
• [X] Flat distributes over dependent pair types
• [X] Flat distributes over product types
• [x] Flat distributes over pullbacks
• [x] ~Flat distributes over sequential limits~
• [x] The unit type is flat discrete

Right exactness of flat

• [X] The empty type is flat discrete
• [X] The natural numbers are flat discrete
• [X] Flat distributes over coproduct types
• [x] ~Flat distributes over pushouts~
• [x] ~Flat distributes over coequalizers~
• [x] ~Flat distributes over sequential colimits~

Notes

• The constructor for the flat modality is renamed from cons-flat to intro-flat. This makes it easier to distinguish from counit-flat.
• In the future, we will probably want to prove crisp-based-ind-Id from the existence of the sharp modality rather than postulating it. The same is true for the modal induction principle of the sharp modality.
• This PR does some ground work with the sharp modality too.

[fredrik-bakke]

I am marking this PR as ready for review, as it is very close to finished. What I have in mind left to complete are a couple of sections of prose that I have specifically tagged with TODOs. While this PR is very low priority, would you at some point be willing to review this @EgbertRijke or perhaps even @VojtechStep?

[EgbertRijke]

Would it be reasonable a separate PR for the changes not in modal-type-theory? Those changes seem quite useful to me and they can be merged today independently of the rest of the PR.

One way to do this is:

• create a new branch from master in your clone

• go into this new branch

• use the following command to pull all the changes from a specific folder into your branch:

  git checkout flat-modality -- path/to/your/folder
  

  where path/to/your/folder ranges over the paths to elementary-number-theory, foundation, foundation-core, and `orthogonal-factorization-systems.

Note that this is only a suggestion. If you prefer to not create a separate pull request for these changes, that's ok with me too.

[fredrik-bakke]

Would it be reasonable a separate PR for the changes not in modal-type-theory? Those changes seem quite useful to me and they can be merged today independently of the rest of the PR.

One way to do this is:

• create a new branch from master in your clone

• go into this new branch

• use the following command to pull all the changes from a specific folder into your branch:

  git checkout flat-modality -- path/to/your/folder
  

  where path/to/your/folder ranges over the paths to elementary-number-theory, foundation, foundation-core, and `orthogonal-factorization-systems.

Note that this is only a suggestion. If you prefer to not create a separate pull request for these changes, that's ok with me too.

Yes! I was thinking the same actually. 😅

[EgbertRijke]

Btw if there is a better way to do this, I would love to know. This was just the one way I know how to create a branch with changes from specific folders, but obviously my git skills are nowhere near as good as the git skills of you and Vojtech.

[fredrik-bakke]

Btw if there is a better way to do this, I would love to know. This was just the one way I know how to create a branch with changes from specific folders, but obviously my git skills are nowhere near as good as the git skills of you and Vojtech.

That's not true. I didn't for instance know how to do this before you instructed me just now.

[fredrik-bakke]

I am marking this PR as ready for review, as it is very close to finished. What I have in mind left to complete are a couple of sections of prose that I have specifically tagged with TODOs. While this PR is very low priority, would you at some point be willing to review this @EgbertRijke or perhaps even @VojtechStep?

I've added the missing explanations mentioned in this comment now.

[fredrik-bakke]

Since it seems no one is willing to give a review of this PR, I'm happy to have it merged without one. If that is okay with you @EgbertRijke @VojtechStep

[EgbertRijke]

I quickly glanced over this PR and it looks good to me. Sorry that this flew under the radar for so long.