Add reference to MRR88 in files about apartness relations (#1128)

UniMath · May 23, 2024 · 20508c1 · 20508c1
1 parent b2a9814
commit 20508c1
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/src/foundation/apartness-relations.lagda.md b/src/foundation/apartness-relations.lagda.md
@@ -220,3 +220,7 @@ module _
   pr2 (pr2 (pr2 (pr2 exp-Type-With-Apartness))) =
     is-cotransitive-apart-function-into-Type-With-Apartness
 ```
+
+## References
+
+{{#bibliography}} {{#reference MRR88}}
diff --git a/src/foundation/standard-apartness-relations.lagda.md b/src/foundation/standard-apartness-relations.lagda.md
@@ -55,3 +55,7 @@ pr1 (is-standard-is-tight-Apartness-Relation R H lem x y) np =
 pr2 (is-standard-is-tight-Apartness-Relation R H lem x .x) r refl =
   antirefl-Apartness-Relation R x r
 ```
+
+## References
+
+{{#bibliography}} {{#reference MRR88}}
diff --git a/src/foundation/tight-apartness-relations.lagda.md b/src/foundation/tight-apartness-relations.lagda.md
@@ -123,3 +123,7 @@ pr1 (exp-Type-With-Tight-Apartness X Y) =
 pr2 (exp-Type-With-Tight-Apartness X Y) =
   is-tight-apartness-function-into-Type-With-Tight-Apartness Y
 ```
+
+## References
+
+{{#bibliography}} {{#reference MRR88}}