Epimorphisms with respect to truncated types

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-26.
Last modified on 2023-06-10.

module foundation.epimorphisms-with-respect-to-truncated-types where
open import foundation.commuting-squares-of-maps
open import foundation.embeddings
open import foundation.functoriality-truncation
open import foundation.truncation-equivalences
open import foundation.truncations
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.truncated-types
open import foundation-core.truncation-levels


A map f : A → B is said to be a k-epimorphism if the precomposition function

  - ∘ f : (B → X) → (A → X)

is an embedding for every k-truncated type X.



is-epimorphism-Truncated-Type :
  {l1 l2 : Level} (l : Level) (k : 𝕋) {A : UU l1} {B : UU l2} 
  (A  B)  UU (l1  l2  lsuc l)
is-epimorphism-Truncated-Type l k f =
  (X : Truncated-Type l k)  is-emb (precomp f (type-Truncated-Type X))


Every k+1-epimorphism is a k-epimorphism

is-epimorphism-is-epimorphism-succ-Truncated-Type :
  {l1 l2 : Level} (l : Level) (k : 𝕋) {A : UU l1} {B : UU l2} (f : A  B) 
  is-epimorphism-Truncated-Type l (succ-𝕋 k) f 
  is-epimorphism-Truncated-Type l k f
is-epimorphism-is-epimorphism-succ-Truncated-Type l k f H X =
  H (truncated-type-succ-Truncated-Type k X)

Every map is a -1-epimorphism

is-neg-one-epimorphism :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  is-epimorphism-Truncated-Type l3 neg-one-𝕋 f
is-neg-one-epimorphism f P =
    ( is-prop-function-type (is-prop-type-Prop P))
    ( is-prop-function-type (is-prop-type-Prop P))

Every k-equivalence is a k-epimorphism

is-epimorphism-is-truncation-equivalence-Truncated-Type :
  {l1 l2 : Level} (l : Level) (k : 𝕋) {A : UU l1} {B : UU l2} (f : A  B) 
  is-truncation-equivalence k f 
  is-epimorphism-Truncated-Type l k f
is-epimorphism-is-truncation-equivalence-Truncated-Type l k f H X =
  is-emb-is-equiv (is-equiv-precomp-is-truncation-equivalence k f H X)

A map is a k-epimorphism if and only if its k-truncation is a k-epimorphism

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

  is-epimorphism-is-epimorphism-map-trunc-Truncated-Type :
    is-epimorphism-Truncated-Type l3 k (map-trunc k f) 
    is-epimorphism-Truncated-Type l3 k f
  is-epimorphism-is-epimorphism-map-trunc-Truncated-Type H X =
      ( precomp (map-trunc k f) (type-Truncated-Type X))
      ( precomp unit-trunc (type-Truncated-Type X))
      ( precomp unit-trunc (type-Truncated-Type X))
      ( precomp f (type-Truncated-Type X))
      ( precomp-coherence-square-maps
        ( unit-trunc)
        ( f)
        ( map-trunc k f)
        ( unit-trunc)
        ( inv-htpy (coherence-square-map-trunc k f))
        ( type-Truncated-Type X))
      ( is-truncation-trunc X)
      ( is-truncation-trunc X)
      ( H X)

Recent changes