search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
450 stars 138 forks source link

Base change, sliced adjoints #1120

Closed marcinjangrzybowski closed 3 weeks ago

felixwellen commented 5 months ago

@marcinjangrzybowski is this ready for review/merging? @maxsnew are you up for reviewing this PR?

marcinjangrzybowski commented 5 months ago

yes, is ready to review, @felixwellen this is prerequisite to "setoids are not LLLC" PR we talked about

maxsnew commented 5 months ago

Sure I can review

marcinjangrzybowski commented 1 month ago

@maxsnew Thank you for review, and sory for not adressing your comments earlier. I think that I addressed all your notes now :)