Add citation — computational identity types (#1191)

Adds explicit citations to Martín Escardó for the constructions of the
involutive and Yoneda identity types.

src/foundation/computational-identity-types.lagda.md

@@ -42,30 +42,33 @@ _weakly_. On this page, we consider the
 {{#concept "computational identity types" Agda=computational-Id}} `x ＝ʲ y`,
 whose elements we call
 {{#concept "computational identifications" Agda=computational-Id}}. These are
-defined using the construction of the
+defined by taking the
 [strictly involutive identity types](foundation.strictly-involutive-identity-types.md):
 
 ```text
   (x ＝ⁱ y) := Σ (z : A) ((z ＝ y) × (z ＝ x))
 ```
 
 but using the [Yoneda identity types](foundation.yoneda-identity-types.md)
-(`_＝ʸ_`) as the underlying identity types:
 
 ```text
   (x ＝ʸ y) := (z : A) → (z ＝ x) → (z ＝ y),
 ```
 
-hence, their definition is
+as the underlying identity types. Both of these underlying constructions are due
+to Martín Escardó {{#cite Esc19DefinitionsEquivalence}}. Hence, the
+_computational identity type_ is
 
 ```text
   (x ＝ʲ y) := Σ (z : A) ((z ＝ʸ y) × (z ＝ʸ x)).
 ```
 
-The Yoneda identity types are [equivalent](foundation-core.equivalences.md) to
-the standard identity types, but have a strictly associative and unital
-concatenation operation. We can leverage this and the strictness properties of
-the construction of the strictly involutive identity types to construct
+Both the strictly involutive identity types and Yoneda identity types are
+[equivalent](foundation-core.equivalences.md) to the standard identity types but
+satisfy further strict algebraic laws. While the strictly involutive identity
+types have a strictly involutive inverse operation and a one-sided unital
+concatenation, the Yoneda identity types have a strictly associative two-sided
+unital concatenation operation. We leverage this to define appropriate
 operations on the computational identity types that satisfy the strict algebraic
 laws
 
@@ -77,10 +80,10 @@ laws
 While the last three equalities hold by the same computations as for the
 strictly involutive identity types using the fact that `invʸ reflʸ ≐ reflʸ`,
 strict associativity relies on the strict associativity of the underlying Yoneda
-identity types. See the file about strictly involutive identity types for
-further details on computations related to the last three equalities. In
-addition to these strict algebraic laws, we also define a recursion principle
-for the computational identity types that computes strictly.
+identity types. See the page on strictly involutive identity types for further
+details on computations related to the last three equalities. In addition to
+these strict algebraic laws, we also have a recursion principle for the
+computational identity types that computes strictly.
 
 **Note.** The computational identity types do _not_ satisfy the strict laws
 
@@ -801,6 +804,10 @@ module _
     is-equiv-map-equiv equiv-computational-eq-equiv
 ```
 
+## References
+
+{{#bibliography}}
+
 ## See also
 
 - [The strictly involutive identity types](foundation.strictly-involutive-identity-types.md)

src/foundation/strictly-involutive-identity-types.lagda.md

@@ -47,8 +47,9 @@ _weakly_. On this page, we consider the
 
 whose elements we call
 {{#concept "strictly involutive identifications" Agda=involutive-Id}}. This type
-family is [equivalent](foundation-core.equivalences.md) to the standard identity
-types, but satisfies the strict laws
+family, due to Martín Escardó {{#cite Esc19DefinitionsEquivalence}}, is
+[equivalent](foundation-core.equivalences.md) to the standard identity types,
+but satisfies the strict laws
 
 - `invⁱ (invⁱ p) ≐ p`
 - `invⁱ reflⁱ ≐ reflⁱ`

src/foundation/yoneda-identity-types.lagda.md

@@ -35,10 +35,11 @@ open import foundation-core.torsorial-type-families
 The standard definition of [identity types](foundation-core.identity-types.md)
 has the limitation that many of the basic operations only satisfy algebraic laws
 _weakly_. On this page, we consider the
-{{#concept "Yoneda identity types" Agda=yoneda-Id}}
+{{#concept "Yoneda identity types" Agda=yoneda-Id}} due to Martín Escardó
+{{#cite Esc19DefinitionsEquivalence}}
 
 ```text
-  (x ＝ʸ y) := (z : A) → (z ＝ x) → (z ＝ y)
+  (x ＝ʸ y) := (z : A) → (z ＝ x) → (z ＝ y).
 ```
 
 Through the interpretation of types as ∞-categories, where the hom-space