Sugar for structs in GATs, example of categories with pushouts

[kris-brown]

There are certain 'derived types' which can in principle be constructed in any GAT but are tedious to do so. Firstly we have equality types, which are witness that two terms are equal. We can implicitly have equations in GAT contexts between generators, but not between general terms. Secondly we have dependent record types, which we call structs.

This PR provides support for directly declaring structs in a theory (which is sugar for a term constructor to make the struct, a type constructor for the type of struct, and projection map term constructors + various expected axioms) and adding equations between terms as arguments to term constructors. The theory of a category with pushouts demonstrates both of these features.

This PR also creates "NonStdLib", which is not exported by GATlab. It's important to distinguish the theories / models which are meant for external consumption (esp. by Catlab) from those which exist purely for testing or pedagogical purposes. (For example, the toy implementation of pushouts in FinSet isn't intended to be efficient.)

Some future work:

• strict=true should check that the equation arguments (as well as implicit equations) for a theory hold.
• Theory maps into / out of theories with structs (+ model migration) needs to be developed and tested, though because we know what they desugar to this requires no new math
• With Eq types, Presentations could possibly be just TypeScopes rather than their own data structure. (A "FreePresentation" could be a presentation without Eq types)

[codecov[bot]]

Codecov Report

Attention: 6 lines in your changes are missing coverage. Please review.

Comparison is base (5bbd879) 95.96% compared to head (2cf56e3) 96.61%.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## migrator #123 +/- ## ============================================ + Coverage 95.96% 96.61% +0.65% ============================================ Files 34 38 +4 Lines 1907 2067 +160 ============================================ + Hits 1830 1997 +167 + Misses 77 70 -7 ``` | [Files](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia) | Coverage Δ | | |---|---|---| | [src/GATlab.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL0dBVGxhYi5qbA==) | `100.00% <ø> (ø)` | | | [src/nonstdlib/models/module.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL25vbnN0ZGxpYi9tb2RlbHMvbW9kdWxlLmps) | `100.00% <100.00%> (ø)` | | | [src/nonstdlib/module.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL25vbnN0ZGxpYi9tb2R1bGUuamw=) | `100.00% <100.00%> (ø)` | | | [src/nonstdlib/theories/module.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL25vbnN0ZGxpYi90aGVvcmllcy9tb2R1bGUuamw=) | `100.00% <100.00%> (ø)` | | | [src/syntax/GATs.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9HQVRzLmps) | `100.00% <ø> (ø)` | | | [src/syntax/TheoryInterface.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9UaGVvcnlJbnRlcmZhY2Uuamw=) | `97.18% <100.00%> (+0.51%)` | :arrow_up: | | [src/syntax/gats/algorithms.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9nYXRzL2FsZ29yaXRobXMuamw=) | `96.46% <100.00%> (+0.95%)` | :arrow_up: | | [src/syntax/gats/ast.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9nYXRzL2FzdC5qbA==) | `91.42% <100.00%> (+5.71%)` | :arrow_up: | | [src/syntax/gats/gat.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9nYXRzL2dhdC5qbA==) | `90.81% <100.00%> (+1.65%)` | :arrow_up: | | [src/syntax/gats/judgments.jl](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia#diff-c3JjL3N5bnRheC9nYXRzL2p1ZGdtZW50cy5qbA==) | `86.66% <100.00%> (+8.09%)` | :arrow_up: | | ... and [3 more](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123?src=pr&el=tree-more&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia) | | ... and [1 file with indirect coverage changes](https://app.codecov.io/gh/AlgebraicJulia/GATlab.jl/pull/123/indirect-changes?src=pr&el=tree-more&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=AlgebraicJulia)

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[olynch]

@kris-brown let's get the codecov up on this, and I'll also try to drop a review soon.

[kris-brown]

thanks, all good points - hopefully all are addressed now!