Martin Escardo

Sets (0-types).

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.Sets where

open import MLTT.Plus-Properties
open import MLTT.Spartan
open import UF.Base
open import UF.Subsingletons

\end{code}

A type is a set if all its identity types are subsingletons. In other
words, sets are types for which equality is a proposition (rather than
data or structure).

\begin{code}

is-h-isolated : {X : ๐ค ฬ } โ X โ ๐ค ฬ
is-h-isolated x = โ {y} โ is-prop (x ๏ผ y)

h-isolatedness-criterion : {X : ๐ค ฬ } {x : X}
โ is-prop (x ๏ผ x)
โ is-h-isolated x
h-isolatedness-criterion {๐ค} {X} {x} i {y} = ฮณ
where
ฮณ : is-prop (x ๏ผ y)
ฮณ refl = i refl

is-set : ๐ค ฬ โ ๐ค ฬ
is-set X = {x : X} โ is-h-isolated x

hSet : (๐ค : Universe) โ ๐ค โบ ฬ
hSet ๐ค = ฮฃ A ๊ ๐ค ฬ , is-set A

underlying-set : hSet ๐ค โ ๐ค ฬ
underlying-set = prโ

underlying-set-is-set : (๐ : hSet ๐ค) โ is-set (underlying-set ๐)
underlying-set-is-set = prโ

๐-is-set : is-set (๐ {๐ค})
๐-is-set {๐ค} {x} = ๐-elim x

refl-is-set : (X : ๐ค ฬ )
โ ((x : X) (p : x ๏ผ x) โ p ๏ผ refl)
โ is-set X
refl-is-set X r {x} p refl = r x p

+-is-set : (X : ๐ค ฬ ) (Y : ๐ฅ ฬ )
โ is-set X
โ is-set Y
โ is-set (X + Y)
+-is-set X Y i j {inl x} {inl x'} p q = ฮณ
where
r : ap inl (inl-lc p) ๏ผ ap inl (inl-lc q)
r = ap (ap inl) (i (inl-lc p) (inl-lc q))

ฮณ : p ๏ผ q
ฮณ = inl-lc-is-section p โ r โ (inl-lc-is-section q)โปยน

+-is-set X Y i j {inl x} {inr y} p q = ๐-elim (+disjoint  p)

+-is-set X Y i j {inr y} {inl x} p q = ๐-elim (+disjoint' p)

+-is-set X Y i j {inr y} {inr y'} p q = ฮณ
where
r : ap inr (inr-lc p) ๏ผ ap inr (inr-lc q)
r = ap (ap inr) (j (inr-lc p) (inr-lc q))

ฮณ : p ๏ผ q
ฮณ = inr-lc-is-section p โ r โ (inr-lc-is-section q)โปยน

ร-is-set : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } โ is-set X โ is-set Y โ is-set (X ร Y)
ร-is-set i j {(x , y)} {(x' , y')} p q =
p            ๏ผโจ tofrom-ร-๏ผ p โฉ
to-ร-๏ผ pโ pโ ๏ผโจ apโ (ฮป -โ -โ โ to-ร-๏ผ -โ -โ) (i pโ qโ) (j pโ qโ) โฉ
to-ร-๏ผ qโ qโ ๏ผโจ (tofrom-ร-๏ผ q)โปยน โฉ
q            โ
where
pโ : x ๏ผ x'
pโ = prโ (from-ร-๏ผ' p)

pโ : y ๏ผ y'
pโ = prโ (from-ร-๏ผ' p)

qโ : x ๏ผ x'
qโ = prโ (from-ร-๏ผ' q)

qโ : y ๏ผ y'
qโ = prโ (from-ร-๏ผ' q)

\end{code}

Formulation of the K axiom for a universe ๐ค.

\begin{code}

K-axiom : โ ๐ค โ ๐ค โบ ฬ
K-axiom ๐ค = (X : ๐ค ฬ ) โ is-set X

K-Axiom : ๐คฯ
K-Axiom = (๐ค : Universe) โ K-axiom ๐ค

\end{code}