Remove private definitions from the library

[EgbertRijke]

Private definitions don't expand outside the module in which they are privately defined, so they should not be used, or be used very sparingly.

[VojtechStep]

For additional details you can consult the following two conversations on the Univalent Agda Discord:

• https://discord.com/channels/954089080197611551/963813799557738536/1113756767197876325
• https://discord.com/channels/954089080197611551/963813799557738536/1114984006954524764