build based on b145299

dev/.documenter-siteinfo.json

@@ -1 +1 @@
-{"documenter":{"julia_version":"1.10.0","generation_timestamp":"2024-01-03T17:18:08","documenter_version":"1.2.1"}}
+{"documenter":{"julia_version":"1.10.0","generation_timestamp":"2024-01-31T00:39:19","documenter_version":"1.2.1"}}

dev/concepts/symbolic_models/index.html

@@ -26,4 +26,4 @@
 end
 A, B, C = [ Ob(CartesianCategoryExprsV2.Ob, X) for X in [:A, :B, :C] ]
 f, g = Hom(:f, A, B), Hom(:g, A, C)
-pair(f, g)</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../models/">« Models and instances</a><a class="docs-footer-nextpage" href="../../api/">Library Reference »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="auto">Automatic (OS)</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.2.1 on <span class="colophon-date" title="Wednesday 3 January 2024 17:18">Wednesday 3 January 2024</span>. Using Julia version 1.10.0.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+pair(f, g)</code></pre></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../models/">« Models and instances</a><a class="docs-footer-nextpage" href="../../api/">Library Reference »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="auto">Automatic (OS)</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.2.1 on <span class="colophon-date" title="Wednesday 31 January 2024 00:39">Wednesday 31 January 2024</span>. Using Julia version 1.10.0.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>

dev/concepts/theories/index.html

@@ -12,4 +12,4 @@
                                 f::(A → B), g::(B → C), h::(C → D)]
   f ⋅ id(B) == f ⊣ [A::Ob, B::Ob, f::(A → B)]
   id(A) ⋅ f == f ⊣ [A::Ob, B::Ob, f::(A → B)]
-end</code></pre><p>The code is simplified only slightly from the official GATlab definition of <code>ThCategory</code>. The theory has two <em>type constructors</em>, <code>Ob</code> (object) and <code>Hom</code> (morphism). The type <code>Hom</code> is a dependent type, depending on two objects, named <code>dom</code> (domain) and <code>codom</code> (codomain). The theory has two <em>term constructors</em>, <code>id</code> (identity) and <code>compose</code> (composition).</p><p>Notice how the return types of the term constructors depend on the argument values. For example, the term <code>id(A)</code> has type <code>Hom(A,A)</code>. The term constructor <code>compose</code> also uses <em>context variables</em>, listed to the right of the <code>⊣</code> symbol. These context variables can also be defined after a <code>where</code> clause, but the left hand side must be surrounded by parentheses. This allows us to write <code>compose(f,g)</code>, instead of the more verbose <code>compose(A,B,C,f,g)</code> (for discussion, see Cartmell, 1986, Sec 10: Informal syntax).</p><p>Notice the <code>@op</code> call where we can create method aliases that can then be used throughout the rest of the theory and outside of definition. We can either use this block notation, or a single line notation such as <code>@op (⋅) := compose</code> to define a single alias. Here we utilize this functionality by replacing the <code>Hom</code> and <code>compose</code> methods with their equivalent Unicode characters, <code>→</code> and <code>⋅</code> respectively. These aliases are also automatically available to definitions that inherit a theory that already has the alias defined.</p><p>The result of the <code>@theory</code> macro is a module with the following members:</p><ol><li><p>For each <em>declaration</em> in the theory (which includes term constructors, type constructors, arguments to type constructors (i.e. accessors like <code>dom</code> and <code>codom</code>), and aliases of the above), a function named with the name of the declaration. These functions are not necessarily original to this module; they may be imported. This allows us to, for instance, use <code>Base.+</code> as a method for a theory. For instance, <code>ThCategory</code> has functions <code>Ob, Hom, dom, codom, compose, id, ⋅, →</code>.</p></li><li><p>A submodule called <code>Meta</code> with members:</p></li></ol><ul><li><code>T</code>: a zero-field struct that serves as a type-level signifier for the theory.</li><li><code>theory</code>: a constant of type <code>GAT</code> which stores the data of the theory.</li><li><code>@theory</code>: a macro which expands directly to <code>theory</code>, which is used to pass around the data of the theory at macro-expand time.</li></ul><div class="admonition is-info"><header class="admonition-header">Note</header><div class="admonition-body"><p>In general, a GAT consists of a <em>signature</em>, defining the types and terms of the theory, and a set of <em>axioms</em>, the equational laws satisfied by models of the theory. The theory of categories, for example, has axioms of unitality and associativity. At present, GATlab supports the specification of both signatures and the axioms, but only uses the axioms as part of  rewriting via e-graphs: it is not automatically checked that models of a GAT satisfy the axioms. It is the responsibility of the programmer to ensure this.</p></div></div><h4 id="References"><a class="docs-heading-anchor" href="#References">References</a><a id="References-1"></a><a class="docs-heading-anchor-permalink" href="#References" title="Permalink"></a></h4><ul><li>Cartmell, 1986: Generalized algebraic theories and contextual categories, <a href="https://doi.org/10.1016/0168-0072(86)90053-9">DOI:10.1016/0168-0072(86)90053-9</a></li><li>Cartmell, 1978, PhD thesis: <em>Generalized algebraic theories and contextual categories</em></li><li>Pitts, 1995: Categorical logic, Sec 6: Dependent types</li></ul></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../scopes/">« Scopes</a><a class="docs-footer-nextpage" href="../models/">Models and instances »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="auto">Automatic (OS)</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.2.1 on <span class="colophon-date" title="Wednesday 3 January 2024 17:18">Wednesday 3 January 2024</span>. Using Julia version 1.10.0.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>
+end</code></pre><p>The code is simplified only slightly from the official GATlab definition of <code>ThCategory</code>. The theory has two <em>type constructors</em>, <code>Ob</code> (object) and <code>Hom</code> (morphism). The type <code>Hom</code> is a dependent type, depending on two objects, named <code>dom</code> (domain) and <code>codom</code> (codomain). The theory has two <em>term constructors</em>, <code>id</code> (identity) and <code>compose</code> (composition).</p><p>Notice how the return types of the term constructors depend on the argument values. For example, the term <code>id(A)</code> has type <code>Hom(A,A)</code>. The term constructor <code>compose</code> also uses <em>context variables</em>, listed to the right of the <code>⊣</code> symbol. These context variables can also be defined after a <code>where</code> clause, but the left hand side must be surrounded by parentheses. This allows us to write <code>compose(f,g)</code>, instead of the more verbose <code>compose(A,B,C,f,g)</code> (for discussion, see Cartmell, 1986, Sec 10: Informal syntax).</p><p>Notice the <code>@op</code> call where we can create method aliases that can then be used throughout the rest of the theory and outside of definition. We can either use this block notation, or a single line notation such as <code>@op (⋅) := compose</code> to define a single alias. Here we utilize this functionality by replacing the <code>Hom</code> and <code>compose</code> methods with their equivalent Unicode characters, <code>→</code> and <code>⋅</code> respectively. These aliases are also automatically available to definitions that inherit a theory that already has the alias defined.</p><p>The result of the <code>@theory</code> macro is a module with the following members:</p><ol><li><p>For each <em>declaration</em> in the theory (which includes term constructors, type constructors, arguments to type constructors (i.e. accessors like <code>dom</code> and <code>codom</code>), and aliases of the above), a function named with the name of the declaration. These functions are not necessarily original to this module; they may be imported. This allows us to, for instance, use <code>Base.+</code> as a method for a theory. For instance, <code>ThCategory</code> has functions <code>Ob, Hom, dom, codom, compose, id, ⋅, →</code>.</p></li><li><p>A submodule called <code>Meta</code> with members:</p></li></ol><ul><li><code>T</code>: a zero-field struct that serves as a type-level signifier for the theory.</li><li><code>theory</code>: a constant of type <code>GAT</code> which stores the data of the theory.</li><li><code>@theory</code>: a macro which expands directly to <code>theory</code>, which is used to pass around the data of the theory at macro-expand time.</li></ul><div class="admonition is-info"><header class="admonition-header">Note</header><div class="admonition-body"><p>In general, a GAT consists of a <em>signature</em>, defining the types and terms of the theory, and a set of <em>axioms</em>, the equational laws satisfied by models of the theory. The theory of categories, for example, has axioms of unitality and associativity. At present, GATlab supports the specification of both signatures and the axioms, but only uses the axioms as part of  rewriting via e-graphs: it is not automatically checked that models of a GAT satisfy the axioms. It is the responsibility of the programmer to ensure this.</p></div></div><h4 id="References"><a class="docs-heading-anchor" href="#References">References</a><a id="References-1"></a><a class="docs-heading-anchor-permalink" href="#References" title="Permalink"></a></h4><ul><li>Cartmell, 1986: Generalized algebraic theories and contextual categories, <a href="https://doi.org/10.1016/0168-0072(86)90053-9">DOI:10.1016/0168-0072(86)90053-9</a></li><li>Cartmell, 1978, PhD thesis: <em>Generalized algebraic theories and contextual categories</em></li><li>Pitts, 1995: Categorical logic, Sec 6: Dependent types</li></ul></article><nav class="docs-footer"><a class="docs-footer-prevpage" href="../scopes/">« Scopes</a><a class="docs-footer-nextpage" href="../models/">Models and instances »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option><option value="auto">Automatic (OS)</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 1.2.1 on <span class="colophon-date" title="Wednesday 31 January 2024 00:39">Wednesday 31 January 2024</span>. Using Julia version 1.10.0.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>