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 :)â†©ï¸Ž