Functoriality of function types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-05-16.
Last modified on 2023-09-14.

module foundation-core.functoriality-function-types where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.type-theoretic-principle-of-choice
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation-core.whiskering-homotopies


Postcomposition preserves homotopies

htpy-postcomp :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (A : UU l3) 
  {f g : X  Y}  (f ~ g)  postcomp A f ~ postcomp A g
htpy-postcomp A H h = eq-htpy (H  h)

compute-htpy-postcomp-refl-htpy :
  {l1 l2 l3 : Level} (A : UU l1) {B : UU l2} {C : UU l3} (f : B  C) 
  (htpy-postcomp A (refl-htpy' f)) ~ refl-htpy
compute-htpy-postcomp-refl-htpy A f h = eq-htpy-refl-htpy (f  h)

The fibers of postcomp

compute-fiber-postcomp :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (A : UU l3) 
  (f : X  Y) (h : A  Y) 
  ((x : A)  fiber f (h x))  fiber (postcomp A f) h
compute-fiber-postcomp A f h =
  equiv-tot  _  equiv-eq-htpy) ∘e distributive-Π-Σ

Precomposition preserves homotopies

htpy-precomp :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {f g : A  B} (H : f ~ g) (C : UU l3) 
  (precomp f C) ~ (precomp g C)
htpy-precomp H C h = eq-htpy (h ·l H)

compute-htpy-precomp-refl-htpy :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) (C : UU l3) 
  (htpy-precomp (refl-htpy' f) C) ~ refl-htpy
compute-htpy-precomp-refl-htpy f C h = eq-htpy-refl-htpy (h  f)

Postcomposition and equivalences

A map f is an equivalence if and only if postcomposing by f is an equivalence

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y)
  (H : {l3 : Level} (A : UU l3)  is-equiv (postcomp A f))

  map-inv-is-equiv-is-equiv-postcomp : Y  X
  map-inv-is-equiv-is-equiv-postcomp = map-inv-is-equiv (H Y) id

  is-section-map-inv-is-equiv-is-equiv-postcomp :
    ( f  map-inv-is-equiv-is-equiv-postcomp) ~ id
  is-section-map-inv-is-equiv-is-equiv-postcomp =
    htpy-eq (is-section-map-inv-is-equiv (H Y) id)

  is-retraction-map-inv-is-equiv-is-equiv-postcomp :
    ( map-inv-is-equiv-is-equiv-postcomp  f) ~ id
  is-retraction-map-inv-is-equiv-is-equiv-postcomp =
      ( ap
        ( pr1)
        ( eq-is-contr
          ( is-contr-map-is-equiv (H X) f)
          { x =
              ( map-inv-is-equiv-is-equiv-postcomp  f)
              ( ap  u  u  f) (is-section-map-inv-is-equiv (H Y) id))}
          { y = pair id refl}))

    is-equiv-is-equiv-postcomp : is-equiv f
    is-equiv-is-equiv-postcomp =

The following version of the same theorem works when X and Y are in the same universe. The condition of inducing equivalences by postcomposition is simplified to that universe.

is-equiv-is-equiv-postcomp' :
  {l : Level} {X : UU l} {Y : UU l} (f : X  Y) 
  ((A : UU l)  is-equiv (postcomp A f))  is-equiv f
  {l} {X} {Y} f is-equiv-postcomp-f =
  let section-f = center (is-contr-map-is-equiv (is-equiv-postcomp-f Y) id)
    ( pr1 section-f)
    ( htpy-eq (pr2 section-f))
    ( htpy-eq
      ( ap
        ( pr1)
        ( eq-is-contr'
          ( is-contr-map-is-equiv (is-equiv-postcomp-f X) f)
          ( pair ((pr1 section-f)  f) (ap  t  t  f) (pr2 section-f)))
          ( pair id refl))))

  is-equiv-postcomp-is-equiv :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y)  is-equiv f 
    {l3 : Level} (A : UU l3)  is-equiv (postcomp A f)
  is-equiv-postcomp-is-equiv {X = X} {Y = Y} f is-equiv-f A =
      ( postcomp A (map-inv-is-equiv is-equiv-f))
      ( eq-htpy  htpy-right-whisk (is-section-map-inv-is-equiv is-equiv-f))
      ( eq-htpy  htpy-right-whisk (is-retraction-map-inv-is-equiv is-equiv-f))

  is-equiv-postcomp-equiv :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y) 
    {l3 : Level} (A : UU l3)  is-equiv (postcomp A (map-equiv f))
  is-equiv-postcomp-equiv f =
    is-equiv-postcomp-is-equiv (map-equiv f) (is-equiv-map-equiv f)

equiv-postcomp :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (A : UU l3) 
  (X  Y)  (A  X)  (A  Y)
pr1 (equiv-postcomp A e) = postcomp A (map-equiv e)
pr2 (equiv-postcomp A e) =
  is-equiv-postcomp-is-equiv (map-equiv e) (is-equiv-map-equiv e) A

Precomposition and equivalences

If dependent precomposition by f is an equivalence, then precomposition by f is an equivalence

  is-equiv-precomp-is-equiv-precomp-Π :
    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    ((C : B  UU l3)  is-equiv (precomp-Π f C)) 
    ((C : UU l3)  is-equiv (precomp f C))
  is-equiv-precomp-is-equiv-precomp-Π f is-equiv-precomp-Π-f C =
    is-equiv-precomp-Π-f  y  C)

If f is an equivalence, then precomposition by f is an equivalence

  is-equiv-precomp-is-equiv :
    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B)  is-equiv f 
    (C : UU l3)  is-equiv (precomp f C)
  is-equiv-precomp-is-equiv f is-equiv-f =
    is-equiv-precomp-is-equiv-precomp-Π f
      ( is-equiv-precomp-Π-is-equiv is-equiv-f)

  is-equiv-precomp-equiv :
    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    (C : UU l3)  is-equiv (precomp (map-equiv f) C)
  is-equiv-precomp-equiv f =
    is-equiv-precomp-is-equiv (map-equiv f) (is-equiv-map-equiv f)

equiv-precomp :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (e : A  B) (C : UU l3) 
  (B  C)  (A  C)
pr1 (equiv-precomp e C) = precomp (map-equiv e) C
pr2 (equiv-precomp e C) =
  is-equiv-precomp-is-equiv (map-equiv e) (is-equiv-map-equiv e) C

If precomposing by f is an equivalence, then f is an equivalence

First, we prove this relative to a subuniverse, such that f is a map between two types in that subuniverse.

module _
  { l1 l2 : Level}
  ( α : Level  Level) (P : (l : Level)  UU l  UU (α l))
  ( A : Σ (UU l1) (P l1)) (B : Σ (UU l2) (P l2)) (f : pr1 A  pr1 B)
  ( H : (l : Level) (C : Σ (UU l) (P l))  is-equiv (precomp f (pr1 C)))

  map-inv-is-equiv-precomp-subuniverse : pr1 B  pr1 A
  map-inv-is-equiv-precomp-subuniverse =
    pr1 (center (is-contr-map-is-equiv (H _ A) id))

  is-section-map-inv-is-equiv-precomp-subuniverse :
    ( f  map-inv-is-equiv-precomp-subuniverse) ~ id
  is-section-map-inv-is-equiv-precomp-subuniverse =
      ( ap
        ( pr1)
        ( eq-is-contr'
          ( is-contr-map-is-equiv (H _ B) f)
          ( ( f  (pr1 (center (is-contr-map-is-equiv (H _ A) id)))) ,
            ( ap
              ( λ (g : pr1 A  pr1 A)  f  g)
              ( pr2 (center (is-contr-map-is-equiv (H _ A) id)))))
          ( id , refl)))

  is-retraction-map-inv-is-equiv-precomp-subuniverse :
    ( map-inv-is-equiv-precomp-subuniverse  f) ~ id
  is-retraction-map-inv-is-equiv-precomp-subuniverse =
    htpy-eq (pr2 (center (is-contr-map-is-equiv (H _ A) id)))

    is-equiv-is-equiv-precomp-subuniverse :
      is-equiv f
    is-equiv-is-equiv-precomp-subuniverse =
        ( map-inv-is-equiv-precomp-subuniverse)
        ( is-section-map-inv-is-equiv-precomp-subuniverse)
        ( is-retraction-map-inv-is-equiv-precomp-subuniverse)

Now we prove the usual statement, without the subuniverse

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

    is-equiv-is-equiv-precomp :
      (f : A  B)  ((l : Level) (C : UU l)  is-equiv (precomp f C)) 
      is-equiv f
    is-equiv-is-equiv-precomp f is-equiv-precomp-f =
        ( λ l  l1  l2)
        ( λ l X  A  B)
        ( A , f)
        ( B , f)
        ( f)
        ( λ l C  is-equiv-precomp-f l (pr1 C))

Corollaries for particular subuniverses

is-equiv-is-equiv-precomp-Prop :
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2)
  (f : type-Prop P  type-Prop Q) 
  ({l : Level} (R : Prop l)  is-equiv (precomp f (type-Prop R))) 
  is-equiv f
is-equiv-is-equiv-precomp-Prop P Q f H =
  is-equiv-is-equiv-precomp-subuniverse id  l  is-prop) P Q f  l  H {l})

is-equiv-is-equiv-precomp-Set :
  {l1 l2 : Level} (A : Set l1) (B : Set l2)
  (f : type-Set A  type-Set B) 
  ({l : Level} (C : Set l)  is-equiv (precomp f (type-Set C))) 
  is-equiv f
is-equiv-is-equiv-precomp-Set A B f H =
  is-equiv-is-equiv-precomp-subuniverse id  l  is-set) A B f  l  H {l})

is-equiv-is-equiv-precomp-Truncated-Type :
  {l1 l2 : Level} (k : 𝕋)
  (A : Truncated-Type l1 k) (B : Truncated-Type l2 k)
  (f : type-Truncated-Type A  type-Truncated-Type B) 
  ({l : Level} (C : Truncated-Type l k)  is-equiv (precomp f (pr1 C))) 
  is-equiv f
is-equiv-is-equiv-precomp-Truncated-Type k A B f H =
    is-equiv-is-equiv-precomp-subuniverse id  l  is-trunc k) A B f
      ( λ l  H {l})

See also

Recent changes