Martin Escardo

Sets (0-types).


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

module UF.Sets where

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


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


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} = ฮณ
  ฮณ : 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 = ฮณ
  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 = ฮณ
  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            โˆŽ
   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)


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


K-axiom : โˆ€ ๐“ค โ†’ ๐“ค โบ ฬ‡
K-axiom ๐“ค = (X : ๐“ค ฬ‡ ) โ†’ is-set X

K-Axiom : ๐“คฯ‰
K-Axiom = (๐“ค : Universe) โ†’ K-axiom ๐“ค