Containers, no h-set assumptions

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

459 stars 141 forks source link

Containers, no h-set assumptions #1141

Open aljungstrom opened 4 months ago

aljungstrom commented 4 months ago

This PR contains a small modification of @stefaniatadama 's code in https://github.com/agda/cubical/pull/1129 . There were some problems with showing that containers are closed under greatest fixed points due to issues with coinduction and the termination checker which forced us to include additional set assumptions. This PR removes those assumptions by introducing a bit of nasty path algebra instead:-)

aljungstrom commented 3 months ago

(This PR depends on #1139)