Martin Escardo 2012.

\begin{code}

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

module FirstProjectionInjective where

open import Equality
open import SetsAndFunctions
open import Injection
open import HSets

π₀-mono : {X : Set} → {Y : X → Set} → (∀{x : X} → hprop(Y x)) → left-cancellable π₀
π₀-mono {X} {Y} f {u} {v} r =
lemma r (π₁ u) (π₁ v) (f(subst {X} {Y} r (π₁ u)) (π₁ v))
where
A : ∀(x x' : X) → x ≡ x' → Set
A x x' r = ∀(y : Y x) → ∀(y' : Y x') → subst r y ≡ y' → (x , y) ≡ (x' , y')

lemma : ∀{x x' : X} → ∀(r : x ≡ x') → A x x' r
lemma = J A (λ x x' y → cong (λ y → (x , y)))

\end{code}

I learned this useful theorem from Thierry Coquand. The idea is
that if the premise holds, this means that Σ \(x : X) → Y x) can
be considered as the subobject of X of elements satisfying Y x,
with the first projection as the monomorphic inclusion into X.

This is a corollary:

\begin{code}

subset-of-hset-is-hset : (X : Set) (Y : X → Set) → hset X → ({x : X} → hprop(Y x)) → hset(Σ \(x : X) → Y x)
subset-of-hset-is-hset X Y h p = subtype-of-hset-is-hset π₀ (π₀-mono p) h

\end{code}