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


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.1 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 1
    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)

  1. Named after a Twitter mutual of mine :)↩︎