Martin Escardo 2011, extended 2018 with more properties of the function pair-fun.

Combining two functions to get a function Ξ£ A β Ξ£ B, and properties of
the resulting function.

\begin{code}

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

module UF.PairFun where

open import MLTT.Spartan
open import TypeTopology.Density

open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Subsingletons

module _ {π€ π₯ π¦ π£}
{X : π€ Μ }
{A : X β π₯ Μ }
{Y : π¦ Μ }
{B : Y β π£ Μ }
(f : X β Y)
(g : (x : X) β A x β B (f x))
where

pair-fun : Ξ£ A β Ξ£ B
pair-fun (x , a) = (f x , g x a)

pair-fun-fiber' : (y : Y) β B y β π€ β π₯ β π¦ β π£ Μ
pair-fun-fiber' y b = Ξ£ (x , a) κ fiber f y , fiber (g x) (transportβ»ΒΉ B a b)

pair-fun-fiber-β : (y : Y) (b : B y)
β fiber pair-fun (y , b)
β pair-fun-fiber' y b
pair-fun-fiber-β  y b = qinveq Ο (Ξ³ , Ξ³Ο , ΟΞ³)
where
Ο : fiber pair-fun (y , b) β pair-fun-fiber' y b
Ο ((x , a) , refl) = (x , refl) , (a , refl)

Ξ³ : pair-fun-fiber' y b β fiber pair-fun (y , b)
Ξ³ ((x , refl) , (a , refl)) = (x , a) , refl

Ξ³Ο : (t : fiber pair-fun (y , b)) β Ξ³ (Ο t) οΌ t
Ξ³Ο ((x , a) , refl) = refl

ΟΞ³ : (s : pair-fun-fiber' y b) β Ο (Ξ³ s) οΌ s
ΟΞ³ ((x , refl) , (a , refl)) = refl

pair-fun-is-embedding : is-embedding f
β ((x : X) β is-embedding (g x))
β is-embedding pair-fun
pair-fun-is-embedding e d (y , b) = h
where
i : is-prop (pair-fun-fiber' y b)
i = subtypes-of-props-are-props'
prβ
(prβ-lc (Ξ» {w} β d (prβ w) (transportβ»ΒΉ B (prβ w) b)))
(e y)

h : is-prop (fiber pair-fun (y , b))
h = equiv-to-prop (pair-fun-fiber-β y b) i

pair-fun-is-vv-equiv : is-vv-equiv f
β ((x : X) β is-vv-equiv (g x))
β is-vv-equiv pair-fun
pair-fun-is-vv-equiv e d (y , b) = h
where
k : is-prop (fiber pair-fun (y , b))
k = pair-fun-is-embedding
(equivs-are-embeddings f (vv-equivs-are-equivs f e))
(Ξ» x β equivs-are-embeddings (g x) (vv-equivs-are-equivs (g x) (d x)))
(y , b)

x : X
x = fiber-point (center (e y))

i : f x οΌ y
i = fiber-identification (center (e y))

w : pair-fun-fiber' y b
w = (center (e y) , center (d x (transportβ»ΒΉ B i b)))

h : is-singleton (fiber pair-fun (y , b))
h = pointed-props-are-singletons (β pair-fun-fiber-β y b ββ»ΒΉ w) k

pair-fun-is-equiv : is-equiv f
β ((x : X) β is-equiv (g x))
β is-equiv pair-fun
pair-fun-is-equiv e d = vv-equivs-are-equivs
pair-fun
(pair-fun-is-vv-equiv
(equivs-are-vv-equivs f e)
(Ξ» x β equivs-are-vv-equivs (g x) (d x)))

pair-fun-dense : is-dense f
β ((x : X) β is-dense (g x))
β is-dense pair-fun
pair-fun-dense i j = contrapositive Ξ³ i
where
Ξ³ : (Ξ£ w κ Ξ£ B , Β¬ fiber pair-fun w) β Ξ£ y κ Y , Β¬ fiber f y
Ξ³ ((y , b) , n) = y , m
where
m : Β¬ fiber f y
m (x , refl) = j x (b , l)
where
l : Β¬ fiber (g x) b
l (a , refl) = n ((x , a) , refl)

open import UF.PropTrunc

module pair-fun-surjection (pt : propositional-truncations-exist) where

open PropositionalTruncation pt
open import UF.ImageAndSurjection pt

pair-fun-is-surjection : is-surjection f
β ((x : X) β is-surjection (g x))
β is-surjection pair-fun
pair-fun-is-surjection s t (y , b) = Ξ³
where
Ξ³ : β (x , a) κ Ξ£ A , (pair-fun (x , a) οΌ y , b)
Ξ³ = β₯β₯-rec β-is-prop
(Ξ» {(x , refl) β β₯β₯-rec β-is-prop
(Ξ» {(a , refl) β β£ (x , a) , refl β£})
(t x b)})
(s y)

pair-fun-equiv : {X : π€ Μ } {A : X β π₯ Μ }
{Y : π¦ Μ } {B : Y β π£ Μ }
(f : X β Y)
β ((x : X) β A x β B (β f β x))
β Ξ£ A β Ξ£ B
pair-fun-equiv f g = pair-fun β f β (Ξ» x β β g x β) ,
pair-fun-is-equiv _ _ β f β-is-equiv (Ξ» x β β g x β-is-equiv)

Ξ£-change-of-variable-embedding : {X : π€ Μ } {Y : π₯ Μ }
(A : X β π¦ Μ ) (g : Y β X)
β is-embedding g
β (Ξ£ y κ Y , A (g y)) βͺ (Ξ£ x κ X , A x)
Ξ£-change-of-variable-embedding A g e = pair-fun g (Ξ» _ β id) ,
pair-fun-is-embedding
g
(Ξ» _ β id)
e
(Ξ» _ β id-is-embedding)

pair-fun-embedding : {X : π€ Μ }
{A : X β π₯ Μ }
{Y : π¦ Μ }
{B : Y β π£ Μ }
β (e : X βͺ Y)
β ((x : X) β A x βͺ B (β e β x))
β Ξ£ A βͺ Ξ£ B
pair-fun-embedding (f , i) g = pair-fun f (Ξ» x β β g x β) ,
pair-fun-is-embedding
f
((Ξ» x β β g x β))
i
(Ξ» x β β g x β-is-embedding)

pair-fun-is-embedding-special : {π€ π₯ π¦ : Universe}
{X : π€ Μ  } {Y : π₯ Μ  } {B : Y β π¦ Μ  }
β (f : X β Y)
β (g : (x : X) β B (f x))
β is-embedding f
β ((y : Y) β is-prop (B y))
β is-embedding (Ξ» x β f x , g x)
pair-fun-is-embedding-special {π€} {π₯} {π¦} {X} {Y} {B} f g f-emb B-is-prop = e
where
k : X β X Γ π {π€}
k = β-sym π-rneutral

k-emb : is-embedding β k β
k-emb = equivs-are-embeddings β k β β k β-is-equiv

h : X β Ξ£ B
h x = f x , g x

g' : (x : X) β π β B (f x)
g' x _ = g x

g'-emb : (x : X) β is-embedding (g' x)
g'-emb x = maps-of-props-are-embeddings (g' x) π-is-prop (B-is-prop (f x))

remark : h οΌ pair-fun f g' β β k β
remark = refl

e : is-embedding h
e = β-is-embedding k-emb (pair-fun-is-embedding f g' f-emb g'-emb)

\end{code}