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}