From a1042ae8f05a70d30b11748f823255bad0932eda Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Tue, 21 Jan 2025 22:37:10 +0100
Subject: [PATCH] fix links

---
 ...-limited-principle-of-omniscience.lagda.md | 21 ++++++++++++++++++-
 src/foundation/pi-0-trivial-maps.lagda.md     |  7 +++++--
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
index 176f5f34cf..e0ef1ebe49 100644
--- a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
+++ b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
@@ -26,7 +26,7 @@ open import foundation-core.sets
 
 </details>
 
-## Statement
+## Idea
 
 The {{#concept "lesser limited principle of omniscience" Agda=LLPO}} (LLPO)
 asserts that for any [sequence](foundation.sequences.md) of
@@ -34,6 +34,10 @@ asserts that for any [sequence](foundation.sequences.md) of
 [at most one](foundation-core.propositions.md) `n`, then either `f n` is false
 for all even `n` or `f n` is false for all odd `n`.
 
+## Definitions
+
+### The small lesser limited principle of omniscience
+
 ```agda
 prop-bool-LLPO : Prop lzero
 prop-bool-LLPO =
@@ -53,6 +57,8 @@ is-prop-bool-LLPO : is-prop bool-LLPO
 is-prop-bool-LLPO = is-prop-type-Prop prop-bool-LLPO
 ```
 
+### The lesser limited principle of omniscience with respect to a universe level
+
 ```agda
 prop-level-LLPO : (l : Level) → Prop (lsuc l)
 prop-level-LLPO l =
@@ -72,6 +78,19 @@ prop-level-LLPO l =
               function-Prop
                 ( is-odd-ℕ n)
                 ( neg-Prop (prop-Decidable-Prop (f n)))))))
+
+level-LLPO : (l : Level) → UU (lsuc l)
+level-LLPO l = type-Prop (prop-level-LLPO l)
+
+is-prop-level-LLPO : {l : Level} → is-prop (level-LLPO l)
+is-prop-level-LLPO {l} = is-prop-type-Prop (prop-level-LLPO l)
+```
+
+### The lesser limited principle of omniscience
+
+```agda
+LLPO : UUω
+LLPO = {l : Level} → level-LLPO l
 ```
 
 ## See also
diff --git a/src/foundation/pi-0-trivial-maps.lagda.md b/src/foundation/pi-0-trivial-maps.lagda.md
index ad4f58ffe5..52a95b2dec 100644
--- a/src/foundation/pi-0-trivial-maps.lagda.md
+++ b/src/foundation/pi-0-trivial-maps.lagda.md
@@ -43,8 +43,11 @@ open import foundation-core.sections
 ## Idea
 
 A [map](foundation-core.function-types.md) is said to be
-{{#concept "π₀-trivial" Disambiguation="map of types" Agda=is-π₀-trivial-map}}
-if its [fibers](foundation-core.fibers-of-maps.md) are π₀-trivial.
+{{#concept "π₀-trivial" Disambiguation="map of types" Agda=is-π₀-trivial-map'}}
+if its [fibers](foundation-core.fibers-of-maps.md) are π₀-trivial. I.e., that
+their [set of connected components](foundation.connected-components.md) is a
+[proposition](foundation-core.propositions.md). Equivalently, a type is
+π₀-trivial if all its elements are [merely equal](foundation.mere-equality.md).
 
 ## Definitions