Ansh
I would also like the powerset to be more universe-level polymorphic: Currently, if A is Type a, then P A is A -> hProp a, even though there are multiple...
`leftright` in `Cubical.Foundations.GroupoidLaws` has the same type as `compPath≡compPath'` in `Cubical.Foundations.Prelude`, and they are provably (but not definitionally) equal.
`preserveIsosF` in `Cubical.Categories.Functor.Properties` and `F-Iso` in `Cubical.Categories.Isomorphism`. I think we should deprecate `preserveIsosF`
I would also like this. Is there a reason it hasnt been implemented yet? because it seems like it would be easy to implement since amy fixed the termination checker....
I read through the discussion but I don't really follow why it was ultimately reverted - it seems the only problem it caused was when trying to define a `Prop`-valued...
Are you planning on merging this soon? It would be nice to have
> One would probably want to use _×C_ unqualified, so one would need an unqualified import as well. Then either the file should be imported as > ```agda > open...
[Cubical.Algebra.LindenbaumTarski](https://agda.github.io/cubical/Cubical.Algebra.LindenbaumTarski.html) could also use this improvement: It starts with defining a preorder `Γ ⊢_⇒_`, and then takes the quotient by its symmetric kernel to get a poset (it also subsequently...
This can be closed now, as #1191 has been merged.
hasn't this been fixed with #1082