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}