Renamings and rewordings OFS

[fredrik-bakke]

Summary

• Implement a new naming scheme for files about local and separated objects at localizations/subuniverses/maps, as discussed with Egbert privately.
• Improve particular wordings in the OFS namespace.
• Add a partial converse to the lemma is-trunc-Σ, computes the fibers of map-Σ and add some coherences between composition and map-Σ.
• Add some basic lemmas about local maps.

[fredrik-bakke]

I'm trying out a new file* naming scheme to specify what structure an object is local at.

[fredrik-bakke]

I'm still unsure about the new naming scheme I'm proposing.

For instance, it will lead to awkward phrasings such as

• morphisms-of-arrows-cartesian-at-reflective-subuniverses/morphisms-of-arrows-cartesian-at-maps
• maps-equivalences-at-reflective-subuniverses/maps-equivalences-at-maps
• maps-connected-at-reflective-subuniverses/maps-connected-at-maps

Perhaps better phrasings are

• cartesian-morphisms-of-arrows-at-reflective-subuniverses/cartesian-morphisms-of-arrows-at-maps
• equivalences-at-reflective-subuniverses/equivalences-at-maps (very weird)
• connected-maps-at-reflective-subuniverses/connected-maps-at-maps (also weird)
• local-types-at-maps