Open rahulc29 opened 11 months ago
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
I agree that hProp
s are not necessarily convenient to work with. My primary motivation for relying on hProp
s 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 asEmbedding→Subset
and the like. It might be possible to isolate the proofs involving powersets in theEmbeddings
module? TheEmbeddings
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 following1. 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
hProp
s are not necessarily convenient to work with. My primary motivation for relying onhProp
s was to not have to duplicate the hProp logic given inCubical.Functions.Logic
. I believe it might be a better idea to rewrite theLogic
module anyway to just keep the actual type and theisProp
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
Fixes #1052 Do note that two definitions had to be rewritten to prevent circular dependencies. I've highlighted them in the comments and marked them as
private
.