Martin Escardo, 27 April 2014

\begin{code}

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

module Prop-indexed-product where

open import SpartanMLTT
open import Sets
open import Equivalence

prop-indexed-product : {X : U} {Y : X → U} → isProp X
→ (a : X) → ((x : X) → Y x) ≃ Y a
prop-indexed-product {X} {Y} hp a = f , (g , fg) , (g , gf)
where
Z = (x : X) → Y x
f : Z → Y a
f z = z a
g : Y a → Z
g y x = transport Y (hp a x) y
lemma : (x : X) → hp x x ≡ refl
lemma x = prop-is-set hp (hp x x) refl
fg : (y : Y a) → transport Y (hp a a) y ≡ y
fg y = ap (λ r → transport Y r y) (lemma a)
gf'' : (z : Z) {x y : X} → x ≡ y → transport Y (hp x y) (z x) ≡ z y
gf'' t {x} refl = ap (λ d → transport Y d (t x)) (lemma x)
gf' : (z : Z) (x : X) → transport Y (hp a x) (z a) ≡ z x
gf' z x = gf'' z (hp a x)
open import FunExt
gf : (z : Z) → g(f z) ≡ z
gf z = funext (gf' z)

prop-indexed-product-one : {X : U} {Y : X → U} → (X → ∅)
→ ((x : X) → Y x) ≃ 𝟙
prop-indexed-product-one {X} {Y} φ = unique-to-𝟙 , (g , fg) , (g , gf)
where
g : 𝟙 → (x : X) → Y x
g * x = unique-from-∅ (φ x)
fg : (u : 𝟙) → * ≡ u
fg * = refl
open import FunExt
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}