Martin Escardo, 27 April 2014

\begin{code}

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

module HProp-indexed-product where

open import HSets
open import Isomorphism
open import Equality
open import SetsAndFunctions

hprop-indexed-product : {X : Set} {Y : X  Set}  hprop X 
                       (a : X)  ((x : X)  Y x)  Y a
hprop-indexed-product {X} {Y} hp a = f , g , fg , gf 
 where
  Z = (x : X)  Y x
  f : Z  Y a
  f z = z a
  g : Y a  Z
  g y x = subst (hp a x) y
  lemma : (x : X)  hp x x  refl
  lemma x = hprop-is-hset hp (hp x x) refl
  fg : (y : Y a)  subst (hp a a) y  y
  fg y = cong  r  subst r y) (lemma a)
  gf'' : (z : Z) {x y : X}  x  y  subst (hp x y) (z x)  z y
  gf'' t {x} refl = cong  d  subst d (t x)) (lemma x)
  gf' : (z : Z) (x : X)  subst (hp a x) (z a)  z x
  gf' z x = gf'' z (hp a x)
  open import Extensionality
  gf : (z : Z)  g(f z)  z
  gf z = funext (gf' z)

hprop-indexed-product-one : {X : Set} {Y : X  Set}  (X  )
                            ((x : X)  Y x)  𝟙
hprop-indexed-product-one {X} {Y} φ = unique-to-𝟙 , g , fg , gf 
 where
  g : 𝟙  (x : X)  Y x
  g * x = unique-from-∅ (φ x)
  fg : (u : 𝟙)  *  u 
  fg * = refl
  open import Extensionality
  gf : (z : (x : X)  Y x)  g *  z
  gf z = funext u
   where
    u : (x : X)  g (unique-to-𝟙 z) x  z x
    u x = unique-from-∅ (φ x)

\end{code}