Skip to content

Commit

Permalink
added observational equality of rational numbers
Browse files Browse the repository at this point in the history
  • Loading branch information
blu-bird committed Dec 22, 2024
1 parent 3ae1f7c commit eda22b0
Showing 1 changed file with 45 additions and 0 deletions.
45 changes: 45 additions & 0 deletions src/elementary-number-theory/equality-rational-numbers.lagda.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# Equality of rational numbers

```agda
module elementary-number-theory.equality-rational-numbers where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.rational-numbers

open import foundation.identity-types
open import foundation.universe-levels

```

</details>

## Idea

An equality predicate is defined by similarity on the underlying integer
fractions. Then we show that this predicate characterizes the identity type of
the rational numbers.

## Definition

```agda
Eq-ℚ : UU lzero
Eq-ℚ x y = sim-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)

refl-Eq-ℚ : (x : ℚ) Eq-ℚ x x
refl-Eq-ℚ q = refl-sim-fraction-ℤ (fraction-ℚ q)

Eq-eq-ℚ : {x y : ℚ} x = y Eq-ℚ x y
Eq-eq-ℚ {x} {.x} refl = refl-Eq-ℚ x

eq-Eq-ℚ : (x y : ℚ) Eq-ℚ x y x = y
eq-Eq-ℚ x y H = equational-reasoning
x = rational-fraction-ℤ (fraction-ℚ x) by inv (is-retraction-rational-fraction-ℚ x)
= rational-fraction-ℤ (fraction-ℚ y) by eq-ℚ-sim-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H
= y by is-retraction-rational-fraction-ℚ y


```

0 comments on commit eda22b0

Please sign in to comment.