Merge branch 'master' into iteration-dependent-functions

HOWTO-INSTALL.md

@@ -303,7 +303,7 @@ below to ensure a smooth setup and workflow. Also, please make sure to follow
 our [coding style](CODINGSTYLE.md) and
 [design principles](DESIGN-PRINCIPLES.md).
 
-### <a name="pre-commit-hooks"></a>Pre-commit hooks and Python dependencies
+### Pre-commit hooks and Python dependencies {#pre-commit-hooks}
 
 The agda-unimath library includes [pre-commit](https://pre-commit.com/) hooks
 that enforce [basic formatting rules](CONTRIBUTING.md). These will inform you of
@@ -333,7 +333,7 @@ Keep in mind that `pre-commit` is also a part of the Continuous Integration
 (CI), so any PR that violates the enforced conventions will be automatically
 blocked from merging.
 
-### <a name="build-website"></a>Building and viewing the website locally
+### Building and viewing the website locally {#build-website}
 
 The build process for the website uses the
 [Rust language](https://www.rust-lang.org/)'s package manager `cargo`. To

references.bib

@@ -1,3 +1,15 @@
+@online{1000+theorems,
+  title  = {1000+ theorems},
+  author = {Freek Wiedijk},
+  url    = {https://1000-plus.github.io/}
+}
+
+@online{100theorems,
+  title  = {Formalizing 100 Theorems},
+  author = {Freek Wiedijk},
+  url    = {https://www.cs.ru.nl/~freek/100/}
+}
+
 @article{AKS15,
   title       = {Univalent Categories and the {{Rezk}} Completion},
   author      = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
@@ -69,7 +81,7 @@ @book{BSCS05
   langid    = {hungarian}
 }
 
-@online{BvDR18,
+@inproceedings{BvDR18,
   title       = {Higher {{Groups}} in {{Homotopy Type Theory}}},
   author      = {Buchholtz, Ulrik and van Doorn, Floris and Rijke, Egbert},
   date        = {2018-02-12},
@@ -79,8 +91,15 @@ @online{BvDR18
   eprinttype  = {arxiv},
   eprintclass = {cs, math},
   abstract    = {We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-L\"of type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.},
-  pubstate    = {preprint},
-  keywords    = {03B15,Computer Science - Logic in Computer Science,F.4.1,Mathematics - Algebraic Topology,Mathematics - Logic}
+  isbn        = {9781450355834},
+  doi         = {10.1145/3209108.3209150},
+  pages       = {205--214},
+  numpages    = {10},
+  location    = {Oxford, United Kingdom},
+  booktitle   = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
+  address     = {New York, NY, USA},
+  publisher   = {Association for Computing Machinery},
+  series      = {LICS '18}
 }
 
 @article{BW23,
@@ -690,6 +709,16 @@ @inproceedings{SvDR20
   keywords  = {higher inductive types,homotopy type theory,sequential colimits}
 }
 
+@misc{Swan24,
+  title         = {Oracle modalities},
+  author        = {Swan, Andrew W},
+  year          = {2024},
+  eprint        = {2406.05818},
+  archiveprefix = {arXiv},
+  eprintclass   = {math},
+  primaryclass  = {math.LO}
+}
+
 @book{SymmetryBook,
   title     = {Symmetry},
   author    = {Bezem, Marc and Buchholtz, Ulrik and Cagne, Pierre and Dundas, Bjørn Ian and Grayson, Daniel R},

scripts/utils/__init__.py

@@ -219,14 +219,21 @@ def get_git_tracked_files():
     git_tracked_files = map(pathlib.Path, git_output.strip().split('\n'))
     return git_tracked_files
 
-
 def get_git_last_modified(file_path):
     try:
         # Get the last commit date for the file
-        output = subprocess.check_output(['git', 'log', '-1', '--format=%at', file_path], stderr=subprocess.DEVNULL)
-        return int(output.strip())
+        output = subprocess.check_output(
+            ['git', 'log', '-1', '--format=%at', file_path],
+            stderr=subprocess.DEVNULL
+        )
+        output_str = output.strip()
+        if output_str:
+            return int(output_str)
+        else:
+            # Output is empty, file may be untracked
+            return os.path.getmtime(file_path)
     except subprocess.CalledProcessError:
-        # If the file is not in git or there's an error, return last modified time according to OS
+        # If the git command fails, fall back to filesystem modification time
         return os.path.getmtime(file_path)
 
 def is_file_modified(file_path):

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -28,8 +28,8 @@ open import foundation.unit-type
 
 ## Idea
 
-The absolute value of an integer is the natural number with the same distance
-from `0`.
+The {{#concept "absolute value" Disambiguation="of an integer" Agda=abs-ℤ}} of
+an integer is the natural number with the same distance from `0`.
 
 ## Definition
 

src/elementary-number-theory/ackermann-function.lagda.md

@@ -14,8 +14,9 @@ open import elementary-number-theory.natural-numbers
 
 ## Idea
 
-The Ackermann function is a fast growing binary operation on the natural
-numbers.
+The
+{{#concept "Ackermann function" WD="Ackermann function" WDID=Q341835 Agda=ackermann}}
+is a fast growing binary operation on the natural numbers.
 
 ## Definition
 

src/elementary-number-theory/binomial-coefficients.lagda.md

@@ -20,8 +20,12 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The binomial coefficient `(n choose k)` measures how many decidable subsets of
-`Fin n` there are of size `k`.
+The
+{{#concept "binomial coefficient" WD="binomial coefficient" WDID=Q209875 Agda=binomial-coefficient-ℕ}}
+`(n choose k)` measures
+[how many decidable subsets](univalent-combinatorics.counting-decidable-subtypes.md)
+of size `k` there are of a
+[finite type](univalent-combinatorics.finite-types.md) of size `n`.
 
 ## Definition
 
@@ -68,3 +72,16 @@ is-one-on-diagonal-binomial-coefficient-ℕ (succ-ℕ n) =
     ( is-one-on-diagonal-binomial-coefficient-ℕ n)
     ( is-zero-binomial-coefficient-ℕ n (succ-ℕ n) (succ-le-ℕ n))
 ```
+
+## See also
+
+- [Binomial types](univalent-combinatorics.binomial-types.md)
+
+## External links
+
+- [Binomial coefficients](https://www.britannica.com/science/binomial-coefficient)
+  at Britannica
+- [Binomial coefficient](https://en.wikipedia.org/wiki/Binomial_coefficient) at
+  Wikipedia
+- [Binomial Coefficient](https://mathworld.wolfram.com/BinomialCoefficient.html)
+  at Wolfram MathWorld

src/elementary-number-theory/catalan-numbers.lagda.md

@@ -22,15 +22,46 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The Catalan numbers are a sequence of natural numbers that occur in several
-combinatorics problems.
+The
+{{#concept "Catalan numbers" WD="Catalan number" WDID=Q270513 OEIS=A000108 Agda=catalan-numbers}}
+$C_n$ is a [sequence](foundation.sequences.md) of
+[natural numbers](elementary-number-theory.natural-numbers.md) that occur in
+several combinatorics problems. The sequence starts
+
+```text
+  n   0   1   2   3   4   5   6
+  Cₙ  1   1   2   5  14  42 132 ⋯
+```
+
+The Catalan numbers may be defined by any of the formulas
+
+1. $C_{n + 1} = \sum_{k = 0}^n C_k C_{n-k}$, with $C_0 = 1$,
+2. $C_n = {2n \choose n} - {2n \choose n + 1}$,
+3. $C_{n+1} = \frac{2(2n+1)}{n+2}C_n$, with $C_0 = 1$,
+4. $C_{n} = \frac{1}{n+1}{2n \choose n}$,
+5. $C_{n} = \frac{(2n)!}{(n+1)!n!}$.
+
+Where $n \choose k$ are
+[binomial coefficients](elementary-number-theory.binomial-coefficients.md) and
+$n!$ is the [factorial function](elementary-number-theory.factorials.md).
 
 ## Definitions
 
+### Inductive sum formula for the Catalan numbers
+
+The Catalan numbers may be defined to be the sequence satisfying $C_0 = 1$ and
+the recurrence relation
+
+$$
+C_{n + 1} = \sum_{k = 0}^n C_k C_{n-k}.
+$$
+
 ```agda
 catalan-numbers : ℕ → ℕ
 catalan-numbers =
-  strong-ind-ℕ (λ _ → ℕ) (succ-ℕ zero-ℕ)
+  strong-ind-ℕ
+    ( λ _ → ℕ)
+    ( 1)
     ( λ k C →
       sum-Fin-ℕ k
         ( λ i →
@@ -45,10 +76,40 @@ catalan-numbers =
                     ( nat-Fin k i)
                     ( k)
                     ( strict-upper-bound-nat-Fin k i))))))
+```
 
+### Binomial difference formula for the Catalan numbers
+
+The Catalan numbers may be computed as a
+[distance](elementary-number-theory.distance-natural-numbers.md) between two
+consecutive binomial coefficients
+
+$$
+C_n = \lvert{2n \choose n} - {2n \choose n + 1}\rvert.
+$$
+
+Since ${2n \choose n}$ in general is larger than or equal to
+${2n \choose n + 1}$, this distance is equal to the difference
+
+$$
+C_n = {2n \choose n} - {2n \choose n + 1}.
+$$
+
+However, we prefer the use of the distance binary operation on natural numbers
+in general at it is a total function on natural numbers, and allows us to skip
+proving this inequality.
+
+```agda
 catalan-numbers-binomial : ℕ → ℕ
 catalan-numbers-binomial n =
   dist-ℕ
     ( binomial-coefficient-ℕ (2 *ℕ n) n)
     ( binomial-coefficient-ℕ (2 *ℕ n) (succ-ℕ n))
 ```
+
+## External links
+
+- [Catalan number](https://en.wikipedia.org/wiki/Catalan_number) at Wikipedia
+- [Catalan Number](https://mathworld.wolfram.com/CatalanNumber.html) at Wolfram
+  MathWorld
+- [A000108](https://oeis.org/A000108) in the OEIS

src/elementary-number-theory/cofibonacci.lagda.md

@@ -30,13 +30,20 @@ open import foundation.universe-levels
 
 ## Idea
 
-The [**cofibonacci sequence**][1] is the unique function G : ℕ → ℕ satisfying
-the property that
+The {{#concept "cofibonacci sequence" Agda=cofibonacci}} is the unique function
+`G : ℕ → ℕ` satisfying the property that
 
 ```text
   div-ℕ (G m) n ↔ div-ℕ m (Fibonacci-ℕ n).
 ```
 
+The sequence starts
+
+```text
+  n   0   1   2   3   4   5   6   7   8   9  10  11  12  13
+  Gₙ  1   3   4   6   5  12   8   6  12  15  10  12   7  24  ⋯
+```
+
 ## Definitions
 
 ### The predicate of being a multiple of the `m`-th cofibonacci number
@@ -141,4 +148,4 @@ is-left-adjoint-cofibonacci m n = {!!}
 
 ## External links
 
-[1]: https://oeis.org/A001177
+- [A001177](https://oeis.org/A001177) in the OEIS

src/elementary-number-theory/distance-natural-numbers.lagda.md

@@ -28,9 +28,11 @@ open import foundation.universe-levels
 
 ## Idea
 
-The distance function between natural numbers measures how far two natural
-numbers are apart. In the agda-unimath library we often prefer to work with
-`dist-ℕ` over the partially defined subtraction operation.
+The
+{{#concept "distance function" Disambiguation="between natural numbers" Agda=dist-ℕ}}
+between [natural numbers](elementary-number-theory.natural-numbers.md) measures
+how far two natural numbers are apart. In the agda-unimath library we often
+prefer to work with `dist-ℕ` over the partially defined subtraction operation.
 
 ## Definition
 

src/elementary-number-theory/eulers-totient-function.lagda.md

@@ -19,7 +19,8 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-**Euler's totient function** `φ : ℕ → ℕ` is the function that maps a
+{{#concept "Euler's totient function" WD="Euler's totient function" WDID=Q190026 Agda=eulers-totient-function-relatively-prime}}
+`φ : ℕ → ℕ` is the function that maps a
 [natural number](elementary-number-theory.natural-numbers.md) `n` to the number
 of
 [multiplicative units modulo `n`](elementary-number-theory.multiplicative-units-standard-cyclic-rings.md).
@@ -57,3 +58,10 @@ eulers-totient-function-relatively-prime n =
 ### Table of files related to cyclic types, groups, and rings
 
 {{#include tables/cyclic-types.md}}
+
+## External links
+
+- [Euler's totient function](https://en.wikipedia.org/wiki/Euler%27s_totient_function)
+  at Wikipedia
+- [Totient Function](https://mathworld.wolfram.com/TotientFunction.html) at
+  Wolfram MathWorld

src/elementary-number-theory/factorials.lagda.md

@@ -21,6 +21,12 @@ open import foundation.identity-types
 
 </details>
 
+## Idea
+
+The {{#concept "factorial" WD="factorial" WDID=Q120976 Agda=factorial-ℕ}} `n!`
+of a number `n`, counts the number of ways to linearly order `n` distinct
+objects.
+
 ## Definition
 
 ```agda
@@ -66,3 +72,8 @@ leq-factorial-ℕ (succ-ℕ n) =
     ( succ-ℕ n)
     ( is-nonzero-factorial-ℕ n)
 ```
+
+## External links
+
+- [Factorial](https://en.wikipedia.org/wiki/Factorial) at Wikipedia
+- [A000142](https://oeis.org/A000142) in the OEIS

src/elementary-number-theory/fermat-numbers.lagda.md

@@ -20,8 +20,8 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-{{#concept "Fermat numbers"}} are numbers of the form $F_n := 2^{2^n}+1$. The
-first five Fermat numbers are
+{{#concept "Fermat numbers" WD="Fermat number" WDID=Q207264 Agda=fermat-number-ℕ}}
+are numbers of the form $F_n := 2^{2^n}+1$. The first five Fermat numbers are
 
 ```text
   3, 5, 17, 257, and 65537.
@@ -72,3 +72,8 @@ recursive-fermat-number-ℕ =
           ( λ i → f (nat-Fin (succ-ℕ n) i) (upper-bound-nat-Fin n i)))
         ( 2))
 ```
+
+## External link
+
+- [Fermat number](https://en.wikipedia.org/wiki/Fermat_number) at Wikipedia
+- [A000215](https://oeis.org/A000215) in the OEIS