Merge branch 'main' into matthew/hlevel-context

CITATION.bib

@@ -0,0 +1,6 @@
+@online{1lab,
+  author = {{The 1Lab Development Team}},
+  title = {{The 1Lab}},
+  url = {https://1lab.dev},
+  year = 2023,
+}

src/1Lab/Classical.lagda.md

@@ -0,0 +1,143 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Bool
+open import Data.Dec
+
+open import Homotopy.Space.Suspension.Properties
+open import Homotopy.Space.Suspension
+```
+-->
+
+```agda
+module 1Lab.Classical where
+```
+
+# The law of excluded middle {defines="LEM law-of-excluded-middle excluded-middle"}
+
+While we do not assume any classical principles in the 1Lab, we can still state
+them and explore their consequences.
+
+The **law of excluded middle** (LEM) is the defining principle of classical logic,
+which states that any proposition is either true or false (in other words,
+[[decidable]]). Of course, assuming this as an axiom requires giving up canonicity:
+we could prove that, for example, any Turing machine either halts or does not halt,
+but this would not give us any computational information.
+
+```agda
+LEM : Type
+LEM = ∀ (P : Ω) → Dec ∣ P ∣
+```
+
+Note that we cannot do without the assumption that $P$ is a proposition: the statement
+that all types are decidable is [[inconsistent with univalence|LEM-infty]].
+
+An equivalent statement of excluded middle is the **law of double negation
+elimination** (DNE):
+
+```agda
+DNE : Type
+DNE = ∀ (P : Ω) → ¬ ¬ ∣ P ∣ → ∣ P ∣
+```
+
+We show that these two statements are equivalent propositions.
+
+```agda
+LEM-is-prop : is-prop LEM
+LEM-is-prop = hlevel!
+
+DNE-is-prop : is-prop DNE
+DNE-is-prop = hlevel!
+
+LEM→DNE : LEM → DNE
+LEM→DNE lem P = Dec-elim _ (λ p _ → p) (λ ¬p ¬¬p → absurd (¬¬p ¬p)) (lem P)
+
+DNE→LEM : DNE → LEM
+DNE→LEM dne P = dne (el (Dec ∣ P ∣) hlevel!) λ k → k (no λ p → k (yes p))
+
+LEM≃DNE : LEM ≃ DNE
+LEM≃DNE = prop-ext LEM-is-prop DNE-is-prop LEM→DNE DNE→LEM
+```
+
+## The axiom of choice {defines="axiom-of-choice"}
+
+The **axiom of choice** is a stronger classical principle which allows us to commute
+propositional truncations past Π types.
+
+```agda
+Axiom-of-choice : Typeω
+Axiom-of-choice =
+  ∀ {ℓ ℓ'} {B : Type ℓ} {P : B → Type ℓ'}
+  → is-set B → (∀ b → is-set (P b))
+  → (∀ b → ∥ P b ∥)
+  → ∥ (∀ b → P b) ∥
+```
+
+Like before, the assumptions that $A$ is a set and $P$ is a family of sets are
+required to avoid running afoul of univalence.
+
+<!--
+```agda
+_ = Fibration-equiv
+```
+-->
+
+An equivalent and sometimes useful statement is that all surjections between sets
+merely have a section. This is essentially jumping to the other side of the
+`fibration equivalence`{.Agda ident=Fibration-equiv}.
+
+```agda
+Surjections-split : Typeω
+Surjections-split =
+  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-set A → is-set B
+  → (f : A → B)
+  → (∀ b → ∥ fibre f b ∥)
+  → ∥ (∀ b → fibre f b) ∥
+```
+
+We show that these two statements are logically equivalent^[they are also
+propositions, but since they live in `Typeω`{.Agda} we cannot easily say that].
+
+```agda
+AC→Surjections-split : Axiom-of-choice → Surjections-split
+AC→Surjections-split ac Aset Bset f =
+  ac Bset (fibre-is-hlevel 2 Aset Bset f)
+
+Surjections-split→AC : Surjections-split → Axiom-of-choice
+Surjections-split→AC ss {P = P} Bset Pset h = ∥-∥-map
+  (Equiv.to (Π-cod≃ (Fibre-equiv P)))
+  (ss (Σ-is-hlevel 2 Bset Pset) Bset fst λ b →
+    ∥-∥-map (Equiv.from (Fibre-equiv P b)) (h b))
+```
+
+We can show that the axiom of choice implies the law of excluded middle;
+this is sometimes known as the Diaconescu-Goodman-Myhill theorem^[not to be confused
+with [[Diaconescu's theorem]] in topos theory].
+
+Given a proposition $P$, we consider the [[suspension]] of $P$: the type $\Sigma P$
+is a set with two points and a path between them if and only if $P$ holds.
+
+Since $\Sigma P$ admits a surjection from the booleans, the axiom of choice merely
+gives us a section $\Sigma P \to 2$.
+
+```agda
+module _ (split : Surjections-split) (P : Ω) where
+  section : ∥ ((x : Susp ∣ P ∣) → fibre 2→Σ x) ∥
+  section = split Bool-is-set (Susp-prop-is-set hlevel!) 2→Σ 2→Σ-surjective
+```
+
+But a section is always injective, and the booleans are [[discrete]], so we can
+prove that $\Sigma P$ is also discrete. Since the path type $N \equiv S$ in $\Sigma P$
+is equivalent to $P$, this concludes the proof.
+
+```agda
+  Discrete-ΣP : Discrete (Susp ∣ P ∣)
+  Discrete-ΣP = ∥-∥-rec (Dec-is-hlevel 1 (Susp-prop-is-set hlevel! _ _))
+    (λ f → Discrete-inj (fst ∘ f) (right-inverse→injective 2→Σ (snd ∘ f))
+                        Discrete-Bool)
+    section
+
+  AC→LEM : Dec ∣ P ∣
+  AC→LEM = Dec-≃ (Susp-prop-path hlevel!) Discrete-ΣP
+```

src/1Lab/Counterexamples/GlobalChoice.lagda.md

@@ -0,0 +1,87 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Bool
+open import Data.Dec
+```
+-->
+
+```agda
+module 1Lab.Counterexamples.GlobalChoice where
+```
+
+# Global choice is inconsistent with univalence {defines="global-choice"}
+
+The principle of **global choice** says that we have a function $\| A \| \to A$ for
+any type $A$. We show that this is inconsistent with univalence.
+
+```agda
+Global-choice : Typeω
+Global-choice = ∀ {ℓ} (A : Type ℓ) → ∥ A ∥ → A
+
+module _ (global-choice : Global-choice) where
+```
+
+The idea will be to apply the global choice operator to a *loop* of types, making
+it contradict itself: since the argument to `global-choice`{.Agda} is a proposition,
+we should get the same answer at both endpoints, so picking a non-trivial loop
+will yield a contradiction.
+
+We pick the loop on `Bool`{.Agda} that swaps the two elements.
+
+```agda
+  swap : Bool ≡ Bool
+  swap = ua (not , not-is-equiv)
+```
+
+The type of booleans is inhabited, so we can apply global choice to it.
+
+```agda
+  Bool-inhabited : ∥ Bool ∥
+  Bool-inhabited = inc false
+
+  b : Bool
+  b = global-choice Bool Bool-inhabited
+```
+
+Since `∥ swap i ∥`{.Agda} is a proposition, we get a loop on `Bool-inhabited`{.Agda}
+over `swap`{.Agda}.
+
+```agda
+  irrelevant : PathP (λ i → ∥ swap i ∥) Bool-inhabited Bool-inhabited
+  irrelevant = is-prop→pathp (λ _ → is-prop-∥-∥) Bool-inhabited Bool-inhabited
+```
+
+Hence `b`{.Agda} negates to itself, which is a contradiction.
+
+```agda
+  b≡[swap]b : PathP (λ i → swap i) b b
+  b≡[swap]b i = global-choice (swap i) (irrelevant i)
+
+  b≡notb : b ≡ not b
+  b≡notb = from-pathp⁻ b≡[swap]b
+
+  ¬global-choice : ⊥
+  ¬global-choice = not-no-fixed b≡notb
+```
+
+## ∞-excluded middle is inconsistent with univalence {defines="LEM-infty"}
+
+As a corollary, we also get that the "naïve" statement of the [[law of excluded
+middle]], saying that *every* type is [[decidable]], is inconsistent with univalence.
+
+First, since $\| A \| \to \neg \neg A$, we get that the naïve formulation of
+double negation elimination is false:
+
+```agda
+¬DNE∞ : (∀ {ℓ} (A : Type ℓ) → ¬ ¬ A → A) → ⊥
+¬DNE∞ dne∞ = ¬global-choice λ A a → dne∞ A (λ ¬A → ∥-∥-rec! ¬A a)
+```
+
+Thus $\rm{LEM}_\infty$, which is equivalent to $\rm{DNE}_\infty$, also fails:
+
+```agda
+¬LEM∞ : (∀ {ℓ} (A : Type ℓ) → Dec A) → ⊥
+¬LEM∞ lem∞ = ¬DNE∞ λ A ¬¬a → Dec-rec id (λ ¬a → absurd (¬¬a ¬a)) (lem∞ A)
+```

src/1Lab/Equiv.lagda.md

@@ -51,6 +51,7 @@ private
     A B : Type ℓ₁
 ```
 
+::: {.definition #fibre}
 A _homotopy fibre_, _fibre_ or _preimage_ of a function `f` at a point
 `y : B` is the collection of all elements of `A` that `f` maps to `y`.
 Since many choices of name are possible, we settle on the one that is
@@ -60,6 +61,7 @@ shortest and most aesthetic: `fibre`{.Agda}.
 fibre : (A → B) → B → Type _
 fibre f y = Σ _ λ x → f x ≡ y
 ```
+:::
 
 A function `f` is an equivalence if every one of its fibres is
 [[contractible]] - that is, for any element `y` in the range, there is

src/1Lab/Extensionality.agda

@@ -1,8 +1,8 @@
 open import 1Lab.Reflection.Signature
 open import 1Lab.Path.IdentitySystem
+open import 1Lab.Function.Embedding
 open import 1Lab.Reflection.HLevel
 open import 1Lab.Reflection.Subst
-open import 1Lab.Equiv.Embedding
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Reflection
 open import 1Lab.Type.Sigma
@@ -290,12 +290,21 @@ iso→extensional
 iso→extensional f ext =
   embedding→extensional (Iso→Embedding f) ext
 
+injection→extensional
+  : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
+  → is-set B
+  → {f : A → B}
+  → (∀ {x y} → f x ≡ f y → x ≡ y)
+  → Extensional B ℓr
+  → Extensional A ℓr
+injection→extensional b-set {f} inj ext =
+  embedding→extensional (f , injective→is-embedding b-set f inj) ext
+
 injection→extensional!
   : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
   → {@(tactic hlevel-tactic-worker) sb : is-set B}
   → {f : A → B}
   → (∀ {x y} → f x ≡ f y → x ≡ y)
   → Extensional B ℓr
   → Extensional A ℓr
-injection→extensional! {sb = b-set} {f} inj ext =
-  embedding→extensional (f , injective→is-embedding b-set f inj) ext
+injection→extensional! {sb = b-set} = injection→extensional b-set

src/1Lab/Equiv/Embedding.lagda.md → src/1Lab/Function/Embedding.lagda.md

@@ -20,7 +20,7 @@ open import 1Lab.Type
 -->
 
 ```agda
-module 1Lab.Equiv.Embedding where
+module 1Lab.Function.Embedding where
 ```
 
 <!--
@@ -46,7 +46,7 @@ $1 \coprod 1$.
 
 To develop this correspondence, we note that, if a map is
 `injective`{.Agda} and its codomain is a [set], then all the
-`fibres`{.Agda} $f^*(x)$ of $f$ are [propositions].
+`fibres`{.Agda ident=fibre} $f^*(x)$ of $f$ are [propositions].
 
 [set]: 1Lab.HLevel.html#is-set
 [propositions]: 1Lab.HLevel.html#is-prop
@@ -158,6 +158,12 @@ monic→is-embedding
 monic→is-embedding {f = f} bset monic =
   injective→is-embedding bset _ λ {x} {y} p →
     happly (monic {C = el (Lift _ ⊤) (λ _ _ _ _ i j → lift tt)} (λ _ → x) (λ _ → y) (funext (λ _ → p))) _
+
+right-inverse→injective
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
+  → {f : A → B} (g : B → A)
+  → is-right-inverse f g → injective f
+right-inverse→injective g rinv {x} {y} p = sym (rinv x) ∙ ap g p ∙ rinv y
 ```
 -->