search

lean-catLogic / formalization

Formalization of Categorical Logic in the Lean proof assistant
https://lean-catLogic.github.io
3 stars 0 forks source link

Diamond modality #2

Closed jacobneu closed 1 year ago

jacobneu commented 1 year ago

Adds example language of PPC + a diamond modality, corresponding to a CCC /w monad.

jacobneu commented 1 year ago

Deleted, renamed to #5