Martin Escardo

\begin{code}

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

module UF.Subsingletons-Properties where

open import MLTT.Spartan
open import UF.Hedberg
open import UF.Sets
open import UF.Subsingletons

props-are-Id-collapsible : {X : 𝓤 ̇ }  is-prop X  Id-collapsible X
props-are-Id-collapsible h {x} {y} =  p  h x y) ,  p q  refl)

props-are-sets : {X : 𝓤 ̇ }  is-prop X  is-set X
props-are-sets h = Id-collapsibles-are-sets (props-are-Id-collapsible h)

singletons-are-sets : {X : 𝓤 ̇ }  is-singleton X  is-set X
singletons-are-sets i = props-are-sets (singletons-are-props i)

identifications-in-props-are-refl : {X : 𝓤 ̇} (i : is-prop X) (x : X)
                                   i x x  refl
identifications-in-props-are-refl i x = props-are-sets i (i x x) refl

transport-over-prop : {X : 𝓤 ̇} {Y : X  𝓥 ̇} {x : X} {y : Y x} (i : is-prop X)
                     transport Y (i x x) y  y
transport-over-prop {𝓤} {𝓥} {X} {Y} {x} {y} i =
 ap  -  transport Y - y) (identifications-in-props-are-refl i x)



\end{code}