anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Well-Definedness Predicate for Morphisms #150

Closed agureev closed 1 year ago

agureev commented 1 year ago

Introduces a well-defp-cat function to Geb and SeqN which takes in a morphism in the appropriate category and either gives true if the morphism is well-defined or produces an error message pointing to the point at which the morphism fails to be well-defined, e.g. appropriate domains and codomains do not coincide for composition of morphisms.