module 1Lab.Type.Pi where

Properties of Π types🔗

This module contains properties of dependent function types, not necessarily organised in any way.

Closure under equivalences🔗

Univalence automatically implies that every type former respects equivalences. However, this theorem is limited to equivalences between types in the same universe. Thus, there are functions to perturb the codomain of a dependent function by an equivalence across universe levels:

Π-cod≃ : ((x : A)  P x  Q x)  ((x : A)  P x)  ((x : A)  Q x)
Π-cod≃ k .fst f x = k x .fst (f x)
Π-cod≃ k .snd .is-eqv f .centre .fst x   = equiv-centre (k x) (f x) .fst
Π-cod≃ k .snd .is-eqv f .centre .snd i x = equiv-centre (k x) (f x) .snd i
Π-cod≃ k .snd .is-eqv f .paths (g , p) i .fst x =
  equiv-path (k x) (f x) (g x , λ j  p j x) i .fst
Π-cod≃ k .snd .is-eqv f .paths (g , p) i .snd j x =
  equiv-path (k x) (f x) (g x , λ k  p k x) i .snd j

Π-dom≃ : (e : B  A)  ((x : A)  P x)  ((x : B)  P (e .fst x))
Π-dom≃ {P = P} e =
  Iso→Equiv λ where
    .fst k x  k (e .fst x)
    .snd .is-iso.inv k x  subst P (e.ε x) (k (e.from x))
    .snd .is-iso.rinv k  funext λ x 
        ap₂ (subst P) (sym (e.zig x))
          (sym (from-pathp (symP (ap k (e.η x)))))
       transport⁻transport (ap P (ap (e .fst) (sym (e.η x)))) (k x)
    .snd .is-iso.linv k  funext λ x 
      ap (subst P _) (sym (from-pathp (symP (ap k (e.ε x)))))
       transport⁻transport (sym (ap P (e.ε x))) _
  where module e = Equiv e

Π-impl-cod≃ : ((x : A)  P x  Q x)  ({x : A}  P x)  ({x : A}  Q x)
Π-impl-cod≃ k .fst f {x} = k x .fst (f {x})
Π-impl-cod≃ k .snd .is-eqv f .centre .fst {x}   = equiv-centre (k x) (f {x}) .fst
Π-impl-cod≃ k .snd .is-eqv f .centre .snd i {x} = equiv-centre (k x) (f {x}) .snd i
Π-impl-cod≃ k .snd .is-eqv f .paths (g , p) i .fst {x} =
  equiv-path (k x) (f {x}) (g {x} , λ j  p j {x}) i .fst
Π-impl-cod≃ k .snd .is-eqv f .paths (g , p) i .snd j {x} =
  equiv-path (k x) (f {x}) (g {x} , λ k  p k {x}) i .snd j

For non-dependent functions, we can easily perturb both domain and codomain:

function≃ : (A  B)  (C  D)  (A  C)  (B  D)
function≃ dom rng = Iso→Equiv the-iso where
  rng-iso = is-equiv→is-iso (rng .snd)
  dom-iso = is-equiv→is-iso (dom .snd)

  the-iso : Iso _ _
  the-iso .fst f x = rng .fst (f (dom-iso .is-iso.inv x))
  the-iso .snd .is-iso.inv f x = rng-iso .is-iso.inv (f (dom .fst x))
  the-iso .snd .is-iso.rinv f =
    funext λ x  rng-iso .is-iso.rinv _
                ap f (dom-iso .is-iso.rinv _)
  the-iso .snd .is-iso.linv f =
    funext λ x  rng-iso .is-iso.linv _
                ap f (dom-iso .is-iso.linv _)

equiv≃ : (A  B)  (C  D)  (A  C)  (B  D)
equiv≃ x y = Σ-ap (function≃ x y) λ f  prop-ext
  (is-equiv-is-prop _) (is-equiv-is-prop _)
   e  ∙-is-equiv (∙-is-equiv ((x e⁻¹) .snd) e) (y .snd))
  λ e  equiv-cancelr ((x e⁻¹) .snd) (equiv-cancell (y .snd) e)

Dependent funext🔗

When the domain and codomain are simple types (rather than a higher shape), paths in function spaces are characterised by funext. We can generalise this to funext-dep, in which the domain and codomain are allowed to be lines of types:

funextP
  :  {A : Type } {B : A  I  Type ℓ₁}
   {f :  a  B a i0} {g :  a  B a i1}
   (∀ a  PathP (B a) (f a) (g a))
   PathP  i   a  B a i) f g
funextP p i x = p x i

funext-dep
  :  {A : I  Type } {B : (i : I)  A i  Type ℓ₁} {f g}
   (  {x₀ x₁} (p : PathP A x₀ x₁)
     PathP  i  B i (p i)) (f x₀) (g x₁) )
   PathP  i  (x : A i)  B i x) f g
funext-dep {A = A} {B} h i x =
  transp  k  B i (coei→i A i x k)) (i  ~ i)
    (h  j  coe A i j x) i)

A slightly wonky cubical argument shows that this function is an equivalence. The complication comes from coe not being definitionally the identity when staying at a variable point in the interval.

funext-dep≃ {A = A} {B} {f} {g} = Iso→Equiv isom where
  open is-iso
  isom : Iso _ _
  isom .fst = funext-dep
  isom .snd .is-iso.inv q p i = q i (p i)

  isom .snd .rinv q m i x =
    transp  k  B i (coei→i A i x (k  m))) (m  i  ~ i) (q i (coei→i A i x m))

  isom .snd .linv h m p i =
    transp  k  B i (lemi→i m k)) (m  i  ~ i) (h  j  lemi→j j m) i)
    where
      lemi→j :  j  coe A i j (p i)  p j
      lemi→j j k = coe-path A  i  p i) i j k

      lemi→i : PathP  m  lemi→j i m  p i) (coei→i A i (p i)) refl
      lemi→i m k = coei→i A i (p i) (m  k)

hetero-homotopy≃homotopy
  : {A : I  Type } {B : (i : I)  Type ℓ₁}
    {f : A i0  B i0} {g : A i1  B i1}

   ({x₀ : A i0} {x₁ : A i1}  PathP A x₀ x₁  PathP B (f x₀) (g x₁))
   ((x₀ : A i0)  PathP B (f x₀) (g (coe0→1 A x₀)))

hetero-homotopy≃homotopy {A = A} {B} {f} {g} = Iso→Equiv isom where
  open is-iso
  isom : Iso _ _
  isom .fst h x₀ = h (SinglP-is-contr A x₀ .centre .snd)
  isom .snd .inv k {x₀} {x₁} p =
    subst  fib  PathP B (f x₀) (g (fib .fst))) (SinglP-is-contr A x₀ .paths (x₁ , p)) (k x₀)

  isom .snd .rinv k = funext λ x₀ 
    ap  α  subst  fib  PathP B (f x₀) (g (fib .fst))) α (k x₀))
      (is-prop→is-set SinglP-is-prop (SinglP-is-contr A x₀ .centre) _
        (SinglP-is-contr A x₀ .paths (SinglP-is-contr A x₀ .centre))
        refl)
     transport-refl (k x₀)

  isom .snd .linv h j {x₀} {x₁} p =
    transp
       i  PathP B (f x₀) (g (SinglP-is-contr A x₀ .paths (x₁ , p) (i  j) .fst)))
      j
      (h (SinglP-is-contr A x₀ .paths (x₁ , p) j .snd))