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