improve documentation of self-variables for record types

Author: mikeshulman

docs/source/codata-types.rst

@@ -32,20 +32,6 @@ That is, we use brackets and bars instead of parentheses and commas.  Moreover,
 It is often helpful to think of a codatatype as akin to an *interface* in an object-oriented programming language, in which case the variable ``x`` is like the ``this`` or ``self`` pointer by which an object refers to itself.  Of course an interface in a simply-typed language does not need a self-pointer to specify the *types* of its methods, but in a dependently typed language it does.  In higher-dimensional type theories, the presence of this variable can be used in other ways than simply accessing previously declared methods, such as in the definition of semi-simplicial types using :ref:`Displayed coinductive types`.
 
 
-Self variables for record types
--------------------------------
-
-The syntax of self variables is also available as an alternative when defining record types.  For instance, the usual sort of Σ-type, as a record with eta-conversion, can also be defined by
-
-.. code-block:: none
-
-   def Σ (A : Type) (B : A → Type) : Type ≔ sig (
-     x .fst : A,
-     x .snd : B (x .fst))
-
-It should be emphasized that this is just a different notation for record types, not a "codatatype with eta-conversion".  At present there is no practical difference, but in the future recursion will be forbidden in record types, even those that use the self-variable notation.
-
-
 Copattern matching
 ------------------
 

docs/source/parametricity.rst

@@ -40,6 +40,12 @@ For codatatypes, we simply use the ordinary syntax, but the "self" variable auto
 
    def Gel (A B : Type) (R : A → B → Type) : Br Type A B ≔ codata [ x .ungel : R x.0 x.1 ]
 
+We can also use :ref:`Self variables for record types`:
+
+.. code-block:: none
+
+   def Gel (A B : Type) (R : A → B → Type) : Br Type A B ≔ sig ( x .ungel : R x.0 x.1 )
+
 We may allow more flexibility in the future, but in practice the current restrictions do not seem very onerous.  For most applications, the above "Gel" record type can simply be defined once and used everywhere, rather than declaring new higher-dimensional types all the time.  Note that because record-types satisfy η-conversion, ``Gel A B R a b`` is definitionally isomorphic to ``R a b``.  Thus, ``Br Type A B`` contains ``A → B → Type`` as a "retract up to definitional isomorphism".  This appears to be sufficient for all applications of internal parametricity.  (``Br Type`` does not itself satisfy any η-conversion rule.)
 
 There is one additional subtlety involving higher-dimensional record and codata types, specifically in their degeneracies.  Since ordinary canonical types are "intrinsically" 0-dimensional, any degeneracy operations on them reduce to a "pure degeneracy" consisting entirely of ``p`` s, e.g. ``M⁽ᵖᵖ⁾⁽²¹⁾`` reduces to simply ``M⁽ᵖᵖ⁾``.  These *pure* degeneracies of canonical types are again canonical types of the same form, as discussed in :ref:`Observational higher dimensions`.

docs/source/record-types.rst

@@ -232,3 +232,17 @@ We now list the opacity attributes, along with how altering the opacity of ``pro
    - ``z`` is printed as ``(a, z .snd)``
 
 For a record type with zero fields, η-expansion prints all of its elements as ``()``, with no difference between labeled and positional.  And for a record type with one field, positional η-expansion prints its elements as ``(_ ≔ a)``.  There is currently no way to cause the projections in an η-expansion to be printed with positional notation such as ``(x .0, x .1)``.
+
+
+Self variables for record types
+-------------------------------
+
+There is an alternative notation for defining record types, using the same syntax of "self variables" that is always used for :ref:`codatatypes <Codatatypes and comatching>`.  See there for more details; as an example, Σ-types can equivalently be defined by
+
+.. code-block:: none
+
+   def Σ (A : Type) (B : A → Type) : Type ≔ sig (
+     x .fst : A,
+     x .snd : B (x .fst))
+
+Note that this is just a different notation for record types, not anything like a "codatatype with eta-conversion".  (At present there is no practical difference, but in the future recursion will be forbidden in record types, even those that use the self-variable notation.)  In addition, self-variable syntax cannot be mixed with the usual syntax for defining record types: any given record type declaration must use one or the other consistently for all of its fields.