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

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

Left exactness of flat

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

Right exactness of flat

• The empty type is flat discrete
• The natural numbers are flat discrete
• Flat distributes over coproduct types
• Flat distributes over pushouts
• Flat distributes over coequalizers
• 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]

I have reviewed the changes to foundation, foundation-core, and elementary-number-theory so far, which seem to have little to do with basic properties of the flat modality. I will review the other changes later.

[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.