diff --git a/src/foundation/computational-identity-types.lagda.md b/src/foundation/computational-identity-types.lagda.md
index 256a877232..dd7b53ac80 100644
--- a/src/foundation/computational-identity-types.lagda.md
+++ b/src/foundation/computational-identity-types.lagda.md
@@ -42,7 +42,7 @@ _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
@@ -50,22 +50,25 @@ defined using the construction of the
 ```
 
 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)
diff --git a/src/foundation/strictly-involutive-identity-types.lagda.md b/src/foundation/strictly-involutive-identity-types.lagda.md
index 78402e0de3..41d8a10e2d 100644
--- a/src/foundation/strictly-involutive-identity-types.lagda.md
+++ b/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ⁱ`
diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 9e873169c8..9f112941a7 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/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