# Truncated maps

```agda
module foundation.truncated-maps where

open import foundation-core.truncated-maps public
```

<details><summary>Imports</summary>

```agda
open import foundation.cones-over-cospans
open import foundation.dependent-pair-types
open import foundation.functoriality-fibers-of-maps
open import foundation.identity-types
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.propositions
open import foundation-core.pullbacks
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
```

</details>

## Properties

### Being a truncated map is a property

```agda
module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-prop-is-trunc-map : (k : 𝕋) (f : A → B) → is-prop (is-trunc-map k f)
  is-prop-is-trunc-map k f = is-prop-Π (λ x → is-prop-is-trunc k (fiber f x))

  is-trunc-map-Prop : (k : 𝕋) → (A → B) → Prop (l1 ⊔ l2)
  pr1 (is-trunc-map-Prop k f) = is-trunc-map k f
  pr2 (is-trunc-map-Prop k f) = is-prop-is-trunc-map k f
```

### Pullbacks of truncated maps are truncated maps

```agda
module _
  {l1 l2 l3 l4 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} {C : UU l3}
  {X : UU l4} (f : A → X) (g : B → X) (c : cone f g C)
  where

  abstract
    is-trunc-is-pullback :
      is-pullback f g c → is-trunc-map k g → is-trunc-map k (pr1 c)
    is-trunc-is-pullback pb is-trunc-g a =
      is-trunc-is-equiv k
        ( fiber g (f a))
        ( map-fiber-cone f g c a)
        ( is-fiberwise-equiv-map-fiber-cone-is-pullback f g c pb a)
        ( is-trunc-g (f a))

abstract
  is-trunc-is-pullback' :
    {l1 l2 l3 l4 : Level} (k : 𝕋)
    {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
    (f : A → X) (g : B → X) (c : cone f g C) →
    is-pullback f g c → is-trunc-map k f → is-trunc-map k (pr1 (pr2 c))
  is-trunc-is-pullback' k f g (pair p (pair q H)) pb is-trunc-f =
    is-trunc-is-pullback k g f
      ( swap-cone f g (triple p q H))
      ( is-pullback-swap-cone f g (triple p q H) pb)
      is-trunc-f
```

### Given a `k`-truncated map from X × Y to Z, if X is `k+1`-truncated, then fixing the first coordinate results in a `k`-truncated map

```agda
is-trunc-map-fix-pr1 :
  {l1 l2 l3 : Level} (k : 𝕋) →
  {X : UU l1} {Y : UU l2} {Z : UU l3} →
  {f : X × Y → Z} (p : is-trunc-map k f) →
  is-trunc (succ-𝕋 k) X  → (x₀ : X) → is-trunc-map k (λ y → f (x₀ , y))
is-trunc-map-fix-pr1 k {f = f} p q x₀ z =
  is-trunc-equiv
    ( k)
    ( Σ (fiber f z) (λ ((x , _) , _) → x ＝ x₀))
    ( equiv-right-swap-Σ ∘e
      equiv-Σ-equiv-base _ equiv-right-swap-Σ ∘e
      equiv-Σ-equiv-base _
        ( inv-left-unit-law-Σ-is-contr
          ( is-torsorial-path' x₀)
          ( x₀ , refl)))
    ( is-trunc-Σ (p z) (λ s → q (pr1 (pr1 s)) x₀))
```

### Given a `k`-truncated map from X × Y to Z, if Y is `k+1`-truncated, then fixing the second coordinate results in a `k`-truncated map

```agda
is-trunc-map-fix-pr2 :
  {l1 l2 l3 : Level} (k : 𝕋) →
  {X : UU l1} {Y : UU l2} {Z : UU l3} →
  {f : X × Y → Z} (p : is-trunc-map k f) →
  is-trunc (succ-𝕋 k) Y  → (y₀ : Y) → is-trunc-map k (λ x → f (x , y₀))
is-trunc-map-fix-pr2 k {f = f} p =
  is-trunc-map-fix-pr1
    ( k)
    (is-trunc-map-comp
      ( k)
      ( f)
      ( λ (y , x) → (x , y))
      ( p)
      ( is-trunc-map-is-equiv k is-equiv-map-commutative-prod))
```