Hilbert’s ε-operators

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Stenholm.

Created on 2022-03-30.
Last modified on 2025-01-07.

module foundation.hilberts-epsilon-operators where
Imports 
open import foundation.functoriality-propositional-truncation
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types

Idea

<a id=“concept-Hilbert’s--operator” class=“concept”>Hilbert’s -operator<a href=“#concept-Hilbert’s--operator”>¶ at a type A is a map

  ε : ║A║₋₁ → A

Some authors also refer to this as split support [KECA17]. Contrary to Hilbert, we will not assume that such an operator exists for each type A.

Definition

ε-operator-Hilbert : {l : Level} → UU l → UU l
ε-operator-Hilbert A = type-trunc-Prop A → A

Properties

The existence of Hilbert’s ε-operators is invariant under equivalences

ε-operator-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  ε-operator-Hilbert X → ε-operator-Hilbert Y
ε-operator-equiv e f =
  (map-equiv e ∘ f) ∘ (map-trunc-Prop (map-inv-equiv e))

ε-operator-equiv' :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  ε-operator-Hilbert Y → ε-operator-Hilbert X
ε-operator-equiv' e f =
  (map-inv-equiv e ∘ f) ∘ (map-trunc-Prop (map-equiv e))

References

[KECA17]
Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science, 03 2017. URL: https://lmcs.episciences.org/3217, arXiv:1610.03346, doi:10.23638/LMCS-13(1:15)2017.

Recent changes