search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

Address review from PR #255 #264

Closed ayberkt closed 2 months ago

ayberkt commented 3 months ago

This PR addresses @tomdjong‘s review from PR #255, which was merged into master before @tomdjong had a chance to review.

ayberkt commented 2 months ago

I have now addressed most of @tomdjong‘s comments from PR #255. The only thing I couldn’t do was to generalize the universes. I think this is harder than it sounds, because it requires quite a few dependencies to be generalized as well. I think I could do this but it will be a nontrivial task in itself, and I have more pressing issues to worry about than the generality of universes.

If @tomdjong is fine with it, I propose we merge this now.

tomdjong commented 2 months ago

@ayberkt Yes, I'm absolutely fine with merging this. I only brought up the generalization because it will only become harder if left until later, but I understand that there are more pressing things to do.

ayberkt commented 2 months ago

I think we can go ahead and merge it then @martinescardo.