open import 1Lab.Equiv.Fibrewise
open import 1Lab.HLevel.Retracts
open import 1Lab.Type.Dec
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HLevel.Sets where

Sets🔗

A set, in HoTT, is a type that validates UIP (uniqueness of equality proofs): Any two proofs of the same equality are equal. There are many ways to prove that a type is a set. An equivalence that is well-known in type theory is that UIP is equivalent to Axiom K:

hasK : Type ℓ → Typeω
hasK A = ∀ {ℓ} {x : A} (P : x ≡ x → Type ℓ) → P refl → (p : x ≡ x) → P p

A type is a Set if, and only if, it satisfies K:

K→is-set : hasK A → is-set A
K→is-set K x y =
  J (λ y p → (q : x ≡ y) → p ≡ q) (λ q → K (λ q → refl ≡ q) refl q)

is-set→K : is-set A → hasK A
is-set→K Aset {x = x} P prefl p = transport (λ i → P (Aset _ _ refl p i)) prefl

Rijke’s Theorem🔗

Another useful way of showing that a type is a set is Rijke’s theorem.¹ Suppose we have the following setup: R is a relation on the elements of A; R x y is always a proposition; R is reflexive, and R x y implies x ≡ y. Then we have that (x ≡ y) ≃ R x y, and by closure of h-levels under equivalences, A is a set.

Rijke-equivalence : {R : A → A → Type ℓ}
                  → (refl : {x : A} → R x x)
                  → (toid : {x y : A} → R x y → x ≡ y)
                  → (is-prop : {x y : A} → is-prop (R x y))
                  → {x y : A} → is-equiv (toid {x} {y})
Rijke-equivalence {A = A} {R = R} refl toid isprop = total→equiv equiv where
  equiv : {x : A} → is-equiv (total {P = R x} {Q = x ≡_} (λ y → toid {x} {y}))
  equiv {x} = is-contr→is-equiv
    (contr (x , refl) λ { (x , q) → Σ-path (toid q) (isprop _ _) })
    (contr (x , λ i → x) λ { (x , q) i → q i , λ j → q (i ∧ j) })

By the characterisation of fibrewise equivalences, it suffices to show that total toid induces an equivalence of total spaces. By J, the total space of x ≡_ is contractible; By toid, and the fact that R is propositional, we can contract the total space of R x to (x , refl).

Rijke-is-set : {R : A → A → Type ℓ}
            → (refl : {x : A} → R x x)
            → (toid : {x y : A} → R x y → x ≡ y)
            → (is-prop : {x y : A} → is-prop (R x y))
            → is-set A
Rijke-is-set refl toid isprop x y =
  equiv→is-hlevel 
    toid (Rijke-equivalence refl toid isprop) isprop

Hedberg’s Theorem🔗

As a consequence of Rijke’s theorem, we get that any type for which we can conclude equality from a double-negated equality is a set:

¬¬-separated→is-set : ({x y : A} → ((x ≡ y → ⊥) → ⊥) → x ≡ y)
                    → is-set A
¬¬-separated→is-set stable = Rijke-is-set (λ x → x refl) stable prop where
  prop : {x y : A} → is-prop ((x ≡ y → ⊥) → ⊥)
  prop p q i x = absurd {A = p x ≡ q x} (p x) i

From this we get Hedberg’s theorem: Any type with decidable equality is a set.

Discrete→is-set : Discrete A → is-set A
Discrete→is-set {A = A} dec = ¬¬-separated→is-set sep where
  sep : {x y : A} → ((x ≡ y → ⊥) → ⊥) → x ≡ y
  sep {x = x} {y = y} ¬¬p with dec x y
  ... | yes p = p
  ... | no ¬p = absurd (¬¬p ¬p)