Symmetry, Geometry, Modality.

This thesis consists of four studies into symmetry and geometry in modal homotopy type theory. First, we prove a higher analogue of Schreier's classificiation of group extensions by means of non-abelian cohomology. Second, we put forward a definition of modal fibration suitable for synthetic algebraic topology, and characterize the modal fibrations for the homotopy type modality as those maps for which the homotopy types of their fibers form a local system on the homotopy type of the base. Third, we put forward a synthetic definition of orbifold, and show that all proper \'etale groupoids are orbifolds in this sense. And fourth, we construct the modal fracture hexagon of a higher group, and use this to derive the differential cohomology hexagon in synthetic differential geometry