Open claims about surjective maps

[fredrik-bakke]

The following claims are waiting to be formalized in foundation.surjective-maps:

• [ ] The type Surjection-Into-Truncated-Type l2 (succ-𝕋 k) A is k-truncated
• [ ] The type of surjections A ↠ B is equivalent to the type of families P of inhabited types over B equipped with an equivalence A ≃ Σ B P