Show that `Connected-Map-Into-Truncated-Type l2 k l A` is `k - l - 2`-truncated

[fredrik-bakke]

The following claims are not yet formalized in foundation.connected-maps:

• The type Connected-Map-Into-Truncated-Type l2 k k A is contractible.

and more generally

• The type Connected-Map-Into-Truncated-Type l2 k l A is k - l - 2-truncated.