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}