Displayed Reasoning changes upstream

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory

MIT License

25 stars 5 forks source link

Displayed Reasoning changes upstream #110

Closed maxsnew closed 2 months ago

maxsnew commented 2 months ago

I just merged this PR upstream, which should help us out but means basically all proofs using the displayed reasoning module need to be updated. Somebody should take care of that. Make sure to build on https://github.com/maxsnew/cubical-categorical-logic/pull/107 which addresses some earlier upstream changes.

hejohns commented 2 months ago

working in #111

hejohns commented 2 months ago

closing with #111