Could some reorganization be done to avoid duplication?

Another thing is that I generally don't like operations that take hProp's as input and produce hProp's if they don't have to. It's often better to have something produce a Type and then have the proof that it is an h-prop separately. The reason being that many times one can do things purely for Type's without any need to pass around the h-prop proofs. A more technical issue is that Agda sometimes get confused and implicit arguments tend to work worse as Agda cannot infer the h-prop proofs... I made a comment about this at some point (https://github.com/agda/cubical/blob/master/Cubical/Functions/Logic.agda#L6) and would be quite happy to delete/rewrite the Logic file... Maybe this could be done as part of reorganization so that you can avoid duplication in this PR?

The main aspect is that Cubical.Functions.Embeddings needs some proofs regarding powersets such as Embedding→Subset and the like. It might be possible to isolate the proofs involving powersets in the Embeddings module? The Embeddings module has many very important lemmata that (in my opinion) should be refactored into logically separate modules. In particular, it is easy to see a characterisation into the following

1. Elementary properties of embeddings
2. Embeddings wrt isomorphisms and equivalences
3. "Embedding-into-X→X" style proofs
4. Miscellaneous (composition, transitivity, universe embeddings)
   I have not included the fibration identity principle and the embedding identity principle since they are already in their separate modules and refactoring them would be rather easy.

I agree that hProps are not necessarily convenient to work with. My primary motivation for relying on hProps was to not have to duplicate the hProp logic given in Cubical.Functions.Logic.
I believe it might be a better idea to rewrite the Logic module anyway to just keep the actual type and the isProp proofs separate.

The main aspect is that Cubical.Functions.Embeddings needs some proofs regarding powersets such as Embedding→Subset and the like. It might be possible to isolate the proofs involving powersets in the Embeddings module? The Embeddings module has many very important lemmata that (in my opinion) should be refactored into logically separate modules. In particular, it is easy to see a characterisation into the following

1. Elementary properties of embeddings

2. Embeddings wrt isomorphisms and equivalences

3. "Embedding-into-X→X" style proofs

4. Miscellaneous (composition, transitivity, universe embeddings)
   I have not included the fibration identity principle and the embedding identity principle since they are already in their separate modules and refactoring them would be rather easy.

I agree that hProps are not necessarily convenient to work with. My primary motivation for relying on hProps was to not have to duplicate the hProp logic given in Cubical.Functions.Logic. I believe it might be a better idea to rewrite the Logic module anyway to just keep the actual type and the isProp proofs separate.

I'm not against splitting Functions.Embeddings into multiple files in a separate directory and then have a file exporting everything if this helps with dependencies. I'm also all for rewriting Functions.Logic. Feel free to have a go at it in this PR!

Sure, I'll have a go at it! :D