diff --git a/src/foundation/apartness-relations.lagda.md b/src/foundation/apartness-relations.lagda.md index baf80f0f6b..ed13a9135d 100644 --- 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 index 6e0f2fabc6..3a3df40ac0 100644 --- 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 index 4939115467..f848664137 100644 --- 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}}