Truncation images of maps
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-07-19.
Last modified on 2023-09-06.
module foundation.truncation-images-of-maps where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.truncations open import foundation.universe-levels open import foundation-core.fibers-of-maps open import foundation-core.identity-types open import foundation-core.truncation-levels
Idea
The k
-truncation image of a map f : A → B
is the type trunc-im k f
that fits in the (k
-connected,k
-truncated) factorization of f
. It is
defined as the type
trunc-im k f := Σ (y : B), type-trunc k (fiber f y)
Definition
module _ {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) where trunc-im : UU (l1 ⊔ l2) trunc-im = Σ B (λ y → type-trunc k (fiber f y)) unit-trunc-im : A → trunc-im pr1 (unit-trunc-im x) = f x pr2 (unit-trunc-im x) = unit-trunc (pair x refl) projection-trunc-im : trunc-im → B projection-trunc-im = pr1
Properties
Characterization of the identity types of k+1
-truncation images
module _ {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (f : A → B) where Eq-unit-trunc-im : A → A → UU (l1 ⊔ l2) Eq-unit-trunc-im x y = trunc-im k (ap f {x} {y}) {- extensionality-trunc-im : (x y : A) → ( unit-trunc-im (succ-𝕋 k) f x = unit-trunc-im (succ-𝕋 k) f y) ≃ ( Eq-unit-trunc-im x y) extensionality-trunc-im x y = ( equiv-tot ( λ q → {!!})) ∘e ( equiv-pair-eq-Σ ( unit-trunc-im (succ-𝕋 k) f x) ( unit-trunc-im (succ-𝕋 k) f y)) -}
Recent changes
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).