update docs

docs/Abstract.html

@@ -29,56 +29,56 @@ <h1 class="title">Abstract contexts structures</h1>
 Nicolas Pouillard.</p>
 <div class="section" id="theory">
 <h1>Theory</h1>
-<p>Categorically, it very simple. Contexts are represented by a set <code class="highlight coq"><span class="n">C</span></code>, a distinguished
-element <code class="highlight coq"><span class="o">∅</span></code> and a binary operation <code class="highlight coq"><span class="o">-</span> <span class="o">+▶</span> <span class="o">-</span></code>. Additionally it has a map representing
-variable <code class="highlight coq"><span class="n">𝓋</span> <span class="o">:</span> <span class="n">C</span> <span class="o">→</span> <span class="n">𝒜</span></code> where <code class="highlight coq"><span class="n">𝒜</span></code> is a sufficiently well-behaved category, typically a
+<p>Categorically, it very simple. Contexts are represented by a set <tt class="docutils literal">C</tt>, a distinguished
+element <tt class="docutils literal">∅</tt> and a binary operation <tt class="docutils literal">- +▶ -</tt>. Additionally it has a map representing
+variable <tt class="docutils literal">𝐯 : C → 𝐀</tt> where <tt class="docutils literal">𝐀</tt> is a sufficiently well-behaved category, typically a
 presheaf category. We then ask that</p>
 <ul class="simple">
-<li><code class="highlight coq"><span class="n">𝓋</span> <span class="o">∅</span> <span class="o">≈</span> <span class="o">⊥</span></code>, where <code class="highlight coq"><span class="o">⊥</span></code> is the initial object in <code class="highlight coq"><span class="n">𝒜</span></code> and</li>
-<li><code class="highlight coq"><span class="n">𝓋</span> <span class="o">(</span><span class="n">Γ</span> <span class="o">+▶</span> <span class="n">Δ</span><span class="o">)</span> <span class="o">≈</span> <span class="n">𝓋</span> <span class="n">Γ</span> <span class="o">+</span> <span class="n">𝓋</span> <span class="n">Δ</span></code> where <code class="highlight coq"><span class="o">+</span></code> is the coproduct in <code class="highlight coq"><span class="n">𝒜</span></code>.</li>
+<li><tt class="docutils literal">𝐯 ∅ ≈ ⊥</tt>, where <tt class="docutils literal">⊥</tt> is the initial object in <tt class="docutils literal">𝐀</tt> and</li>
+<li><tt class="docutils literal">𝐯 (Γ +▶ Δ) ≈ 𝐯 Γ + 𝐯 Δ</tt> where <code class="highlight coq"><span class="o">+</span></code> is the coproduct in <tt class="docutils literal">𝐀</tt>.</li>
 </ul>
-<p>Our category of contexts is basically the image of <code class="highlight coq"><span class="n">𝓋</span></code>, which has the structure of a
-commutative monoid. Then, given a family <code class="highlight coq"><span class="n">𝒳</span> <span class="o">:</span> <span class="n">C</span> <span class="o">→</span> <span class="n">𝒜</span></code>, it is easy to define
+<p>Our category of contexts is basically the image of <tt class="docutils literal">𝐯</tt>, which has the structure of a
+commutative monoid. Then, given a family <tt class="docutils literal">X : C → 𝐀</tt>, it is easy to define
 assignments as:</p>
-<pre class="literal-block">
-Γ =[𝒳]&gt; Δ ≔ 𝒜[ 𝓋 Γ , 𝒳 Δ ]
+<pre class="code literal-block">
+Γ =[X]&gt; Δ ≔ 𝐀[ 𝐯 Γ , X Δ ]
 </pre>
 <p>And renamings as:</p>
-<pre class="literal-block">
-Γ ⊆ Δ ≔ Γ =[ 𝓋 ]&gt; Δ
-      ≔ 𝒜[ 𝓋 Γ , 𝓋 Δ ]
+<pre class="code literal-block">
+Γ ⊆ Δ ≔ Γ =[ 𝐯 ]&gt; Δ
+      ≔ 𝐀[ 𝐯 Γ , 𝐯 Δ ]
 </pre>
-<p>Assuming <code class="highlight coq"><span class="n">𝒜</span></code> is (co-)powered over <code class="highlight coq"><span class="kt">Set</span></code>, the substitution tensor product and substitution
-internal hom in <code class="highlight coq"><span class="n">C</span> <span class="o">→</span> <span class="n">𝒜</span></code> are given by:</p>
-<pre class="literal-block">
-( 𝒳 ⊗ 𝒴 ) Γ ≔ ∫^Δ  𝒳 Δ × (Δ =[ 𝒴 ]&gt; Γ)
-⟦ 𝒳 , 𝒴 ⟧ Γ ≔ ∫_Δ  (Γ =[ 𝒳 ]&gt; Δ) → 𝒴 Δ
+<p>Assuming <tt class="docutils literal">𝐀</tt> is (co-)powered over <tt class="docutils literal">Set</tt>, the substitution tensor product and substitution
+internal hom in <tt class="docutils literal">C → 𝐀</tt> are given by:</p>
+<pre class="code literal-block">
+( X ⊗ Y ) Γ ≔ ∫^Δ  X Δ × (Δ =[ Y ]&gt; Γ)
+⟦ X , Y ⟧ Γ ≔ ∫_Δ  (Γ =[ X ]&gt; Δ) → Y Δ
 </pre>
-<p>More generally, given a category <code class="highlight coq"><span class="n">ℬ</span></code> (co-)powered over <code class="highlight coq"><span class="kt">Set</span></code> we can define the the
+<p>More generally, given a category <tt class="docutils literal">𝐁</tt> (co-)powered over <tt class="docutils literal">Set</tt> we can define the the
 following functors, generalizing the substitution tensor and hom to heretogeneous
 settings:</p>
-<pre class="literal-block">
-( - ⊗ - ) : (C → ℬ) → (C → 𝒜) → (C → ℬ)
-( 𝒳 ⊗ 𝒴 ) Γ ≔ ∫^Δ  𝒳 Δ × (Δ =[ 𝒴 ]&gt; Γ)
+<pre class="code literal-block">
+( - ⊗ - ) : (C → 𝐁) → (C → 𝐀) → (C → 𝐁)
+( X ⊗ Y ) Γ ≔ ∫^Δ  X Δ × (Δ =[ Y ]&gt; Γ)
 
-⟦ - , - ⟧ : (C → 𝒜) → (C → ℬ) → (C → ℬ)
-⟦ 𝒳 , 𝒴 ⟧ Γ ≔ ∫_Δ  (Γ =[ 𝒳 ]&gt; Δ) → 𝒴 Δ
+⟦ - , - ⟧ : (C → 𝐀) → (C → 𝐁) → (C → 𝐁)
+⟦ X , Y ⟧ Γ ≔ ∫_Δ  (Γ =[ X ]&gt; Δ) → Y Δ
 </pre>
 </div>
 <div class="section" id="concretely">
 <h1>Concretely</h1>
-<p>We here apply the above theory to the case where <code class="highlight coq"><span class="n">𝓐</span></code> is the family category <code class="highlight coq"><span class="n">T</span> <span class="o">→</span> <span class="kt">Set</span></code> for
-some set <code class="highlight coq"><span class="n">T</span></code>. Taking <code class="highlight coq"><span class="n">T</span></code> to the set of types of some object language, families <code class="highlight coq"><span class="n">C</span> <span class="o">→</span> <span class="n">𝒜</span></code>, ie
-<code class="highlight coq"><span class="n">C</span> <span class="o">→</span> <span class="n">T</span> <span class="o">→</span> <span class="kt">Set</span></code>, model nicely well-scoped and well-typed families. To capture non-typed
-syntactic categories, indexed only by a scope, we develop the special case where <code class="highlight coq"><span class="n">ℬ</span></code> is
-just <code class="highlight coq"><span class="kt">Set</span></code>.</p>
+<p>We here apply the above theory to the case where <tt class="docutils literal">𝐀</tt> is the family category <tt class="docutils literal">T → Set</tt>
+for some set <tt class="docutils literal">T</tt>. Taking <tt class="docutils literal">T</tt> to the set of types of some object language, families
+<tt class="docutils literal">C → 𝐀</tt>, ie <tt class="docutils literal">C → T → Set</tt>, model nicely well-scoped and well-typed families. To
+capture non-typed syntactic categories, indexed only by a scope, we develop the special
+case where <tt class="docutils literal">𝐁</tt> is just <tt class="docutils literal">Set</tt>.</p>
 <p>We then instanciate this abstract structure with the usual lists and DeBruijn indices,
-but also with two useful instances: the direct sum, where the notion of variables <code class="highlight coq"><span class="n">𝓋</span></code> is
-the pointwise coproduct and the subset, where the notion of variables is preserved.</p>
+but also with two useful instances: the direct sum, where the notion of variables <tt class="docutils literal">𝐯</tt>
+is the pointwise coproduct and the subset, where the notion of variables is preserved.</p>
 <p>In further work we wish to tacle this in more generality, notable treating the case for
-the idiomatic presentation of well-scoped untyped syntax where <code class="highlight coq"><span class="n">𝒜</span></code> is <code class="highlight coq"><span class="kt">Set</span></code>, <code class="highlight coq"><span class="n">C</span></code> is <code class="highlight coq"><span class="n">ℕ</span></code>
-and <code class="highlight coq"><span class="n">𝓋</span></code> is <code class="highlight coq"><span class="n">Fin</span></code>. Currently, we do treat untyped syntax, but using the non-idiomatic
-&quot;unityped&quot; presentation.</p>
+the idiomatic presentation of well-scoped untyped syntax where <tt class="docutils literal">𝐀</tt> is <tt class="docutils literal">Set</tt>, <tt class="docutils literal">C</tt>
+is <tt class="docutils literal">ℕ</tt> and <tt class="docutils literal">𝐯</tt> is <tt class="docutils literal">Fin</tt>. Currently, we do treat untyped syntax, but using the
+non-idiomatic &quot;unityped&quot; presentation.</p>
 <p>The first part of the context structure: the distinguished empty context, the binary
 concatenation and the family of variables.</p>
 <pre class="alectryon-io highlight"><!-- Generator: Alectryon --><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Class</span> <span class="nf">context</span> (<span class="nv">T</span> <span class="nv">C</span> : <span class="kt">Type</span>) := {