Classifying invertible maps

[maybemabeline]

I showed that the type of invertible maps is equivalent to the type of equivalences, together with a loop at the underlying map, as discussed with Egbert. Input on the name "looped equivalence" is welcome, as I'm not sure if I like it very much.

[fredrik-bakke]

This is a cool result by the way. Thanks for formalizing it! :)
We can use it to prove the instructive results that

• The type of invertibility proofs is an n-type when the codomain is an n+1-type.
• By extension, the type of invertible maps is equivalent to the type of equivalences when the codomain is a set.
• Not every type of invertibility proofs is an n-type when the codomain is not an n+1-type.

[EgbertRijke]

This is a cool result by the way. Thanks for formalizing it! :) We can use it to prove the instructive results that

• The type of invertibility proofs is an n-type when the codomain is an n+1-type.
• By extension, the type of invertible maps is equivalent to the type of equivalences when the codomain is a set.
• Not every type of invertibility proofs is an n-type when the codomain is not an n+1-type.

This current result shows that the type of invertible maps from A to B is equivalent to the type of maps from the circle into A ≃ B, by the universal property of the circle. Mabel will extend this result to showing that the type of all invertible maps in a universe UU is equivalent to the type of maps from the 2-sphere into the universe UU. This is also why she used identifications and not homotopies of equivalences.

[fredrik-bakke]

Gotcha, very cool!

[EgbertRijke]

Great! If you make that one change about Sigma types in the informal text, and update this branch with master, than this PR will be ready to merge. This is a very nice pull request!