Skip to content

Commit

Permalink
Update src/foundation/discrete-relations.lagda.md
Browse files Browse the repository at this point in the history
Co-authored-by: Fredrik Bakke <[email protected]>
  • Loading branch information
EgbertRijke and fredrik-bakke authored Nov 14, 2024
1 parent 774d2ae commit bf7aab7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/foundation/discrete-relations.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -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),

Expand Down

0 comments on commit bf7aab7

Please sign in to comment.