search

ToposInstitute / CatColab

A collaborative environment for formal, interoperable, conceptual modeling
https://catcolab.org
MIT License
11 stars 4 forks source link

Validate morphisms between models of discrete double theories #104

Closed epatters closed 2 days ago

epatters commented 1 month ago

Follow-up task to #103. Validation should follow the pattern already established for graph morphisms.

kris-brown commented 6 days ago

I noticed there is no graph morphism validation error for having extra data in the map. Is this by design?

epatters commented 6 days ago

It's not by design; I didn't even think about it :) Now that I am thinking about it, I'm not sure whether it should be an error. Maybe it's fine? What do you think?

Also CC @olynch who has been thinking about dependent types as a relation between the base and the total type.

kris-brown commented 6 days ago

I'm fine either way, but it reminds me of the @acset macro which used to silently ignore any misspelled words, e.g. Employe=3. I'm also imagining programmatically generating the vectors for the components of a graph mapping and, due to some conceptual error, we're producing vectors larger than they need to be. It might be nicer to get an error of the "index error" kind than a "unnatural mapping" kind.

epatters commented 6 days ago

I'm persuaded by that, especially given that CatColab is supposed to be designed to give informative error messages!

kris-brown commented 6 days ago

I guess this only makes sense for finitely presented graph morphisms / model morphisms - the general interface just exposes how it acts on objects, so it wouldn't make sense to test for 'extra data'.