Martin Escardo 2012. 


{-# 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))
  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)))

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:


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