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)

  1. Named after a Twitter mutual of mine :)β†©οΈŽ