You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have a personal project building a model of set theory in agda, following the HoTT book chapter 10.5. The current status is just a gist lying around. Are you interested in a pull request? If so, what would be the best way to structure this to fit into the cubical library (none of the top-level directories seem applicable)? Also note that at one point I make use of the {-# TERMINATING #-} pragma, I'm not so sure how to get rid of that.
The text was updated successfully, but these errors were encountered:
* first port to standard library
* getting rid of TERMINATING, now --safe
* moved last helper
* fix typos
* deduplicate isProp→isContrPathP
* split cumulative hierarchy
* fix line lengths
* simplifying isPropMonicPresentation
* fixup from library changes
* update to cubical master
* Update Properties.agda
Co-authored-by: ecavallo <ecavallo@cs.cmu.edu>
Co-authored-by: Anders Mörtberg <andersmortberg@gmail.com>
I have a personal project building a model of set theory in agda, following the HoTT book chapter 10.5. The current status is just a gist lying around. Are you interested in a pull request? If so, what would be the best way to structure this to fit into the cubical library (none of the top-level directories seem applicable)? Also note that at one point I make use of the
{-# TERMINATING #-}
pragma, I'm not so sure how to get rid of that.The text was updated successfully, but these errors were encountered: