Skip to content

Commit

Permalink
Update src/foundation/apartness-relations.lagda.md
Browse files Browse the repository at this point in the history
Co-authored-by: Egbert Rijke <[email protected]>
  • Loading branch information
fredrik-bakke and EgbertRijke authored Oct 9, 2023
1 parent bbf5037 commit 1c1240a
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/foundation/apartness-relations.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,9 @@ open import foundation-core.propositions
An **apartness relation** on a type `A` is a
[relation](foundation.binary-relations.md) `R` which is

- **Antireflexive**: For any `a : A` we have `¬ (R a a)`
- **Symmetric**: For any `a b : A` we have `R a b R b a`
- **Cotransitive**: For any `a b c : A` we have `R a b R a c ∨ R b c`.
- **Antireflexive:** For any `a : A` we have `¬ (R a a)`
- **Symmetric:** For any `a b : A` we have `R a b R b a`
- **Cotransitive:** For any `a b c : A` we have `R a b R a c ∨ R b c`.

The idea of an apartness relation `R` is that `R a b` holds if you can
positively establish a difference between `a` and `b`. For example, two subsets
Expand Down

0 comments on commit 1c1240a

Please sign in to comment.