# Functoriality of truncations

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Stenholm and Tom de Jong.

Created on 2022-06-15.

module foundation.functoriality-truncation where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.truncations
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.retractions
open import foundation-core.retracts-of-types
open import foundation-core.sections
open import foundation-core.truncation-levels


## Idea

The universal property of truncations can be used to define the functorial action of truncations.

## Definition

module _
{l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B)
where

unique-map-trunc :
is-contr
( Σ ( type-trunc k A → type-trunc k B)
( coherence-square-maps f unit-trunc unit-trunc))
unique-map-trunc =
universal-property-trunc k A (trunc k B) (unit-trunc ∘ f)

map-trunc : type-trunc k A → type-trunc k B
map-trunc = pr1 (center unique-map-trunc)

coherence-square-map-trunc :
coherence-square-maps f unit-trunc unit-trunc map-trunc
coherence-square-map-trunc = pr2 (center unique-map-trunc)


## Properties

### Truncations of homotopic maps are homotopic

naturality-unit-trunc :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (k : 𝕋) (f : A → B) →
map-trunc k f ∘ unit-trunc ~ unit-trunc ∘ f
naturality-unit-trunc k f = pr2 (center (unique-map-trunc k f))

htpy-uniqueness-map-trunc :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (k : 𝕋) (f : A → B) →
(h : type-trunc k A → type-trunc k B) →
h ∘ unit-trunc ~ unit-trunc ∘ f → map-trunc k f ~ h
htpy-uniqueness-map-trunc k f h H =
htpy-eq (ap pr1 (contraction (unique-map-trunc k f) (h , H)))

htpy-trunc :
{l1 l2 : Level} {A : UU l1} {B : UU l2} {k : 𝕋} {f g : A → B} →
f ~ g → map-trunc k f ~ map-trunc k g
htpy-trunc {k = k} {f} {g} H =
htpy-uniqueness-map-trunc
( k)
( f)
( map-trunc k g)
( naturality-unit-trunc k g ∙h inv-htpy (unit-trunc ·l H))


### The truncation of the identity map is the identity map

id-map-trunc : {l1 : Level} {A : UU l1} (k : 𝕋) → map-trunc k (id {A = A}) ~ id
id-map-trunc k = htpy-uniqueness-map-trunc k id id refl-htpy


### The truncation of a composite is the composite of the truncations

preserves-comp-map-trunc :
{ l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (k : 𝕋)
( g : B → C) (f : A → B) →
( map-trunc k (g ∘ f)) ~
( (map-trunc k g) ∘ (map-trunc k f))
preserves-comp-map-trunc k g f =
htpy-uniqueness-map-trunc k
( g ∘ f)
( map-trunc k g ∘ map-trunc k f)
( ( map-trunc k g ·l naturality-unit-trunc k f) ∙h
( naturality-unit-trunc k g ·r f))


### The functorial action of truncations preserves equivalences

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (k : 𝕋) (e : A ≃ B)
where

map-equiv-trunc : type-trunc k A → type-trunc k B
map-equiv-trunc = map-trunc k (map-equiv e)

map-inv-equiv-trunc : type-trunc k B → type-trunc k A
map-inv-equiv-trunc = map-trunc k (map-inv-equiv e)

is-equiv-map-equiv-trunc : is-equiv map-equiv-trunc
is-equiv-map-equiv-trunc =
is-equiv-is-invertible
( map-inv-equiv-trunc)
( inv-htpy
( preserves-comp-map-trunc k (map-equiv e) (map-inv-equiv e)) ∙h
( htpy-trunc (is-section-map-inv-equiv e) ∙h id-map-trunc k))
( inv-htpy
( preserves-comp-map-trunc k (map-inv-equiv e) (map-equiv e)) ∙h
( htpy-trunc (is-retraction-map-inv-equiv e) ∙h id-map-trunc k))

equiv-trunc : (type-trunc k A ≃ type-trunc k B)
pr1 equiv-trunc = map-equiv-trunc
pr2 equiv-trunc = is-equiv-map-equiv-trunc


### Truncations preserve retracts

module _
{l1 l2 : Level} {k : 𝕋} {A : UU l1} {B : UU l2}
where

section-map-trunc-section :
(f : A → B) → section f → section (map-trunc k f)
pr1 (section-map-trunc-section f S) =
map-trunc k (map-section f S)
pr2 (section-map-trunc-section f (s , h)) =
homotopy-reasoning
map-trunc k f ∘ map-trunc k s
~ map-trunc k (f ∘ s)
by inv-htpy (preserves-comp-map-trunc k f s)
~ map-trunc k id
by htpy-eq (ap (map-trunc k) (eq-htpy h))
~ id
by id-map-trunc k

retraction-map-trunc-retraction :
(f : A → B) → retraction f → retraction (map-trunc k f)
pr1 (retraction-map-trunc-retraction f S) =
map-trunc k (map-retraction f S)
pr2 (retraction-map-trunc-retraction f (r , h)) =
homotopy-reasoning
map-trunc k r ∘ map-trunc k f
~ map-trunc k (r ∘ f)
by inv-htpy (preserves-comp-map-trunc k r f)
~ map-trunc k id
by htpy-eq (ap (map-trunc k) (eq-htpy h))
~ id
by id-map-trunc k

retract-of-trunc-retract-of :
A retract-of B → (type-trunc k A) retract-of (type-trunc k B)
pr1 (retract-of-trunc-retract-of R) =
map-trunc k (inclusion-retract R)
pr2 (retract-of-trunc-retract-of R) =
retraction-map-trunc-retraction
( inclusion-retract R)
( retraction-retract R)