From bf7aab7c1aa0a1d0c6eeea4615e87ddeb11fd6fe Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 14 Nov 2024 14:41:49 -0500 Subject: [PATCH] Update src/foundation/discrete-relations.lagda.md Co-authored-by: Fredrik Bakke --- src/foundation/discrete-relations.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/discrete-relations.lagda.md b/src/foundation/discrete-relations.lagda.md index 3ed3b137a2..ffa8015d23 100644 --- a/src/foundation/discrete-relations.lagda.md +++ b/src/foundation/discrete-relations.lagda.md @@ -30,7 +30,7 @@ if, for every element `x : A`, the type family `R x` is [contractible](foundation-core.contractible-types.md) for every `x`. The -{{#concept "standard discrete relation" Disambiguation="binary relations valued in types"}} +{{#concept "standard discrete relation" Disambiguation="reflexive relations valued in types"}} on a type `X` is the relation defined by [identifications](foundation-core.identity-types.md),