search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
26 stars 5 forks source link

Update UMP.agda, NaturalModels/, Syntax/ to build again #91

Open hejohns opened 6 months ago

hejohns commented 6 months ago

In 325c84bd0d6d8aa73f529e6efb9753046f8da84c, files under NaturalModels, Syntax, and UMP.agda were removed because they didn't build anymore.

Fix-up UMP.agda and the other files.

https://github.com/maxsnew/cubical-categorical-logic/pull/90#issuecomment-2119326787

hejohns commented 6 months ago

For convenience, I've attached the git revert patch to 325c84bd0d6d8aa73f529e6efb9753046f8da84c. Although, owing to

Note: If you use Linux and try to upload a .patch file, you will receive an error message. This is a known issue.

https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/attaching-files

I've attached it as a .md. It's really a git format-patch -n HEAD^1. 0001-Revert-remove-everything-that-doesn-t-build-and-make.md

maxsnew commented 3 months ago

I'm working on reformulating some of this stuff to use elimination principles etc to see if we can more directly apply our gluing techniques to lambda calculi viewed as free simple categories with families rather than free CCCs