fix links

UniMath · Jan 21, 2025 · a1042ae · a1042ae
1 parent 77381ec
commit a1042ae
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 3 deletions.
diff --git a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
@@ -26,14 +26,18 @@ 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
 [booleans](foundation.booleans.md) `f : ℕ → bool` such that `f n` is true for
 [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
@@ -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