Martin Escardo 2012.

\begin{code}

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

module FirstProjectionInjective where

open import SpartanMLTT
open import Injection
open import Sets

pr₁-mono : {X : U} {Y : X → U} → ({x : X} → isProp(Y x)) → left-cancellable pr₁
pr₁-mono {X} {Y} f {u} {v} r =
lemma r (pr₂ u) (pr₂ v) (f(transport Y r (pr₂ u)) (pr₂ v))
where
A : (x x' : X) → x ≡ x' → U
A x x' r = (y : Y x) (y' : Y x') → transport Y r y ≡ y' → (x , y) ≡ (x' , y')

lemma : {x x' : X} (r : x ≡ x') → A x x' r
lemma = J A (λ x x' y → ap (λ 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-set-is-set : (X : U) (Y : X → U) → isSet X → ({x : X} → isProp(Y x)) → isSet(Σ \(x : X) → Y x)
subset-of-set-is-set X Y h p = subtype-of-set-is-set pr₁ (pr₁-mono p) h

\end{code}