Skip to content

Commit

Permalink
Merge branch 'master' into refactor-up-limits
Browse files Browse the repository at this point in the history
  • Loading branch information
@fredrik-bakke
fredrik-bakke authored Dec 7, 2023
2 parents d4e5457 + ab24893 commit ded7a94
Show file tree
Hide file tree
Showing 21 changed files with 1,263 additions and 111 deletions.
38 changes: 20 additions & 18 deletions MIXFIX-OPERATORS.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ Below, we outline a list of general rules when assigning associativities.
associated regardless. For instance, one should never write

```agda
assoc : p ∙ (q ∙ r) ＝ p ∙ q ∙ r
assoc : p ∙ q ∙ r ＝ p ∙ (q ∙ r)
```

- **Unique well-typed associativity**. When an operator only has one well-typed
Expand All @@ -163,20 +163,22 @@ Below, we outline a list of general rules when assigning associativities.

## Full table of assigned precedences

| Precedence level | Operators |
| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| 50 | Unary non-parametric operators. This class is currently empty |
| 45 | Exponentiative arithmetic operators |
| 40 | Multiplicative arithmetic operators |
| 36 | Subtractive arithmetic operators |
| 35 | Additive arithmetic operators |
| 30 | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_` |
| 25 | Parametric unary operators. This class is currently empty |
| 20 | Parametric exponentiative operators. This class is currently empty |
| 15 | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, identification concatenation and whiskering operators like `_∙_`, `_∙h_`, `_·l_`, and `_·r_` |
| 10 | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad |
| 6 | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, and `_↔_`, elementhood relations, subtype relations |
| 5 | Directed function type-like formation operators, e.g. `_→∗_` and `_↪_` |
| 3 | The pairing operators `_,_` and `_,ω_` |
| 0-1 | Reasoning syntaxes |
| -∞ | Function type formation `_→_` |
| Precedence level | Operators |
| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| 50 | Unary non-parametric operators. This class is currently empty |
| 45 | Exponentiative arithmetic operators |
| 40 | Multiplicative arithmetic operators |
| 36 | Subtractive arithmetic operators |
| 35 | Additive arithmetic operators |
| 30 | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_` |
| 25 | Parametric unary operators. This class is currently empty |
| 20 | Parametric exponentiative operators. This class is currently empty |
| 17 | Left homotopy whiskering `_·l_` |
| 16 | Right homotopy whiskering `_·r_` |
| 15 | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` |
| 10 | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad |
| 6 | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, and `_↔_`, elementhood relations, subtype relations |
| 5 | Directed function type-like formation operators, e.g. `_→∗_` and `_↪_` |
| 3 | The pairing operators `_,_` and `_,ω_` |
| 0-1 | Reasoning syntaxes |
| -∞ | Function type formation `_→_` |
3 changes: 3 additions & 0 deletions src/elementary-number-theory.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ open import elementary-number-theory.collatz-conjecture public
open import elementary-number-theory.commutative-semiring-of-natural-numbers public
open import elementary-number-theory.congruence-integers public
open import elementary-number-theory.congruence-natural-numbers public
open import elementary-number-theory.cubes-natural-numbers public
open import elementary-number-theory.decidable-dependent-function-types public
open import elementary-number-theory.decidable-total-order-natural-numbers public
open import elementary-number-theory.decidable-total-order-standard-finite-types public
Expand Down Expand Up @@ -55,6 +56,7 @@ open import elementary-number-theory.greatest-common-divisor-integers public
open import elementary-number-theory.greatest-common-divisor-natural-numbers public
open import elementary-number-theory.group-of-integers public
open import elementary-number-theory.half-integers public
open import elementary-number-theory.hardy-ramanujan-number public
open import elementary-number-theory.inequality-integer-fractions public
open import elementary-number-theory.inequality-integers public
open import elementary-number-theory.inequality-natural-numbers public
Expand Down Expand Up @@ -120,6 +122,7 @@ open import elementary-number-theory.strict-inequality-natural-numbers public
open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
open import elementary-number-theory.strong-induction-natural-numbers public
open import elementary-number-theory.sums-of-natural-numbers public
open import elementary-number-theory.taxicab-numbers public
open import elementary-number-theory.telephone-numbers public
open import elementary-number-theory.triangular-numbers public
open import elementary-number-theory.twin-prime-conjecture public
Expand Down
58 changes: 58 additions & 0 deletions src/elementary-number-theory/cubes-natural-numbers.lagda.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
# Cubes of natural numbers

```agda
module elementary-number-theory.cubes-natural-numbers where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.squares-natural-numbers

open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.universe-levels
```

</details>

## Idea

The {{#concept "cube" Disambiguation="natural number"}} `n³` of a
[natural number](elementary-number-theory.natural-numbers.md) `n` is the triple
[product](elementary-number-theory.multiplication-natural-numbers.md)

```text
n³ := n * n * n
```

of `n` with itself.

## Definitions

### Cubes of natural numbers

```agda
cube-ℕ : ℕ → ℕ
cube-ℕ n = square-ℕ n *ℕ n
```

### The predicate of being a cube of natural numbers

```agda
is-cube-ℕ : ℕ → UU lzero
is-cube-ℕ = fiber cube-ℕ
```

### The cubic root of cubic natural numbers

```agda
cubic-root-ℕ : (n : ℕ) → is-cube-ℕ n → ℕ
cubic-root-ℕ n = pr1
```

## See also

- [Squares of natural numbers](elementary-number-theory.squares-natural-numbers.md)
73 changes: 73 additions & 0 deletions src/elementary-number-theory/hardy-ramanujan-number.lagda.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
# The Hardy-Ramanujan number

```agda
module elementary-number-theory.hardy-ramanujan-number where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.taxicab-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unit-type
```

</details>

## Idea

The
{{#concept "Hardy-Ramanujan number" Agda=Hardy-Ramanujan-ℕ WD="1729" WDID=Q825176}}
is the number `1729`. This number is the second
[taxicab number](elementary-number-theory.taxicab-numbers.md), i.e., it is the
least natural number that can be written as a sum of cubes of positive natural
numbers in exactly two distinct ways. Specifically, we have the identifications

```text
1³ + 12³ ＝ 1729 and 9³ + 10³ ＝ 1729.
```

## Definition

### The Hardy-Ramanujan number

```agda
Hardy-Ramanujan-ℕ : ℕ
Hardy-Ramanujan-ℕ = 1729
```

## Properties

### Two decompositions of the Hardy-Ramanujan number into sums of cubes of two positive natural numbers

```agda
first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ :
sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ
pr1 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ =
(1 , is-nonzero-one-ℕ)
pr1 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) =
(12 , is-nonzero-succ-ℕ 11)
pr1 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
star
pr2 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
refl

second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ :
sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ
pr1 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ =
(9 , is-nonzero-succ-ℕ 8)
pr1 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) =
(10 , is-nonzero-succ-ℕ 9)
pr1 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
star
pr2 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) =
refl
```

## External links

- [1729 (number)](<https://en.wikipedia.org/wiki/1729_(number)>) at Wikipedia
18 changes: 18 additions & 0 deletions src/elementary-number-theory/multiplication-natural-numbers.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,19 @@ open import foundation.negated-equality

</details>

## Idea

The {{#concept "multiplication" Disambiguation="natural numbers"}} operation on
the [natural numbers](elementary-number-theory.natural-numbers.md) is defined by
[iteratively](foundation.iterating-functions.md) applying
[addition](elementary-number-theory.addition-natural-numbers.md) of a number to
itself. More preciesly the number `m * n` is defined by adding the number `n` to
itself `m` times:

```text
m * n = n + ⋯ + n (n added to itself m times).
```

## Definition

### Multiplication
Expand Down Expand Up @@ -239,3 +252,8 @@ neq-mul-ℕ m n p =
( ( right-successor-law-mul-ℕ (succ-ℕ m) (succ-ℕ n)) ∙
( ap ((succ-ℕ m) +ℕ_) (left-successor-law-mul-ℕ m (succ-ℕ n)))))
```

## See also

- [Squares of natural numbers](elementary-number-theory.squares-natural-numbers.md)
- [Cubes of natural numbers](elementary-number-theory.cubes-natural-numbers.md)
27 changes: 25 additions & 2 deletions src/elementary-number-theory/squares-natural-numbers.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,18 +28,37 @@ open import foundation-core.transport-along-identifications

</details>

## Idea

The {{#concept "square" Disambiguation="natural number"}} `n²` of a
[natural number](elementary-number-theory.natural-numbers.md) `n` is the
[product](elementary-number-theory.multiplication-natural-numbers.md)

```text
n² := n * n
```

of `n` with itself.

## Definition

### Squares of natural numbers

```agda
square-ℕ : ℕ → ℕ
square-ℕ n = mul-ℕ n n
```

cube-ℕ : ℕ → ℕ
cube-ℕ n = (square-ℕ n) *ℕ n
### The predicate of being a square of a natural number

```agda
is-square-ℕ : ℕ → UU lzero
is-square-ℕ n = Σ ℕ (λ x → n ＝ square-ℕ x)
```

### The square root of a square natural number

```agda
square-root-ℕ : (n : ℕ) → is-square-ℕ n → ℕ
square-root-ℕ _ (root , _) = root
```
Expand Down Expand Up @@ -153,3 +172,7 @@ is-decidable-is-square-ℕ n =
( λ x → has-decidable-equality-ℕ n (square-ℕ x))
( is-decidable-big-root n)
```

## See also

- [Cubes of natural numbers](elementary-number-theory.cubes-natural-numbers.md)
104 changes: 104 additions & 0 deletions src/elementary-number-theory/taxicab-numbers.lagda.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
# Taxicab numbers

```agda
module elementary-number-theory.taxicab-numbers where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.cubes-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.nonzero-natural-numbers

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types
```

</details>

## Idea

The `n`-th
{{#concept "taxicab number" Agda=is-taxicab-number-ℕ WD="taxicab number" WDID=Q1462591}}
`taxicab n` is the smallest
[natural number](elementary-number-theory.natural-numbers.md) `x` such that `x`
is a [sum](elementary-number-theory.addition-natural-numbers.md) of two
[cubes](elementary-number-theory.cubes-natural-numbers.md) in `n`
[distinct](foundation.negated-equality.md) ways.

**Note:** The definition of taxicab numbers only considers sums of
[positive integers](elementary-number-theory.nonzero-natural-numbers.md). Note
that if `n` is a cube, i.e., if `n ＝ c³`, then the only solutions to the
equation

```text
a³ + b³ = c³
```

have either `a ＝ 0` or `b ＝ 0` by
[Fermat's last theorem](https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem).
Therefore `n` can be written in at least two different ways as a sum of cubes of
positive natural numbers if and only if it can be written in at least two
different ways as a sum of cubes of arbitary natural numbers. However, the class
of natural numbers that can be written in exactly one way as a sum of cubes is
different when we consider sums of cubes of positive natural numbers or sums of
cubes of arbitrary natural numbers.

## Definitions

### The type of decompositions of a natural number as a sum of cubes

```agda
sum-of-cubes-decomposition-ℕ : ℕ → UU lzero
sum-of-cubes-decomposition-ℕ x =
Σ ( nonzero-ℕ)
( λ y →
Σ ( nonzero-ℕ)
( λ z →
( leq-ℕ (nat-nonzero-ℕ y) (nat-nonzero-ℕ z)) ×
( cube-ℕ (nat-nonzero-ℕ y) +ℕ cube-ℕ (nat-nonzero-ℕ z) ＝ x)))
```

### The predicate of being a sum of two cubes in exactly `n` distinct ways

A number `x` is a sum of cubes in `n` distinct ways if there is an equivalence

```text
Fin n ≃ sum-of-cubes-decomposition-ℕ x
```

from the
[standard finite type](univalent-combinatorics.standard-finite-types.md) to the
type `sum-of-cubes-decomposition-ℕ x` of ways of writing `x` as a sum of cubes.

```agda
is-sum-of-cubes-in-number-of-distinct-ways-ℕ : ℕ → ℕ → UU lzero
is-sum-of-cubes-in-number-of-distinct-ways-ℕ n x =
Fin n ≃ sum-of-cubes-decomposition-ℕ x
```

### The predicate of being the `n`-th taxicab number

```agda
is-taxicab-number-ℕ : ℕ → ℕ → UU lzero
is-taxicab-number-ℕ n x =
is-sum-of-cubes-in-number-of-distinct-ways-ℕ n x ×
((y : ℕ) → is-sum-of-cubes-in-number-of-distinct-ways-ℕ n y → leq-ℕ x y)
```

## See also

- [The Hardy-Ramanujan number](elementary-number-theory.hardy-ramanujan-number.md)

## External links

- [Taxicab numbers](https://en.wikipedia.org/wiki/Taxicab_number) at Wikipedia
- [Taxicab nubmers](https://oeis.org/A011541) at the OEIS.
Loading

0 comments on commit ded7a94

Please sign in to comment.