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}