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}