Formalize the Hopf Fibration

[morphismz]

Construct the hopf fibration in such a way that the generator of $\mathbb{S}^3$ is sent to a 3-loop in $\mathbb{S}^2$ constructed using Eckmann-Hilton.

A detailed plan for this may be too much to write out in a comment here. But I'll list a few components that will go into this.

Done or currently being worked on:

• finish dependent universal property of suspensions
• "Universal Property of Fibers of maps": build up infrastructure for working with the family of fibers of a map f : A --> B as the initial type family equipped with a section (a : A) --> fib_f (f a).
  Open tasks
• show EH is (more or less) the naturality condition of whiskering a 2-path on the left by a 1-path
• "Eckmann-Hilton in the universe" idea: show that tr sends EH on identifications to EH on homotopies (almost done, missing a few coherences)

Open:

• descent for $\mathbb{S}^1$, $\mathbb{S}^2$, $\mathbb{S}^3$
  ----- related to issue Postulating colimits #1122 . This proof works best the the point and n-loop presentation of spheres, which have yet to be postulated.
• characterizing (higher) homotopies between (homotopies) functions with domain $\mathbb{S}^1$,
• characterizing homotopies between dependent functions functions with domain $\mathbb{S}^3$.

Quasi-references:

• a talk presenting the current version of the proof https://morphismz.github.io/talks/2024-04-03-hottuf