Epimorphisms with respect to maps into sets

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.

Created on 2022-02-17.
Last modified on 2023-06-10.

module foundation.epimorphisms-with-respect-to-sets where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.epimorphisms-with-respect-to-truncated-types
open import foundation.existential-quantification
open import foundation.function-extensionality
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.surjective-maps
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.truncation-levels
open import foundation-core.univalence


An epimorphism with respect to maps into sets are maps f : A → B suc that for every set C the precomposition function (B → C) → (A → C) is an embedding.


is-epimorphism-Set :
  {l1 l2 : Level} (l : Level) {A : UU l1} {B : UU l2}
  (f : A  B)  UU (l1  l2  lsuc l)
is-epimorphism-Set l f =
  is-epimorphism-Truncated-Type l zero-𝕋 f


Surjective maps are epimorphisms with respect to maps into sets

  is-epimorphism-is-surjective-Set :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
    is-surjective f  {l : Level}  is-epimorphism-Set l f
  is-epimorphism-is-surjective-Set H C =
      ( is-set-function-type (is-set-type-Set C))
      ( λ {g} {h} p 
        eq-htpy  b 
            ( H b)
            ( Id-Prop C (g b) (h b))
            ( λ u 
              ( inv (ap g (pr2 u))) 
              ( ( htpy-eq p (pr1 u)) 
                ( ap h (pr2 u))))))

Maps that are epimorphisms with respect to maps into sets are surjective

  is-surjective-is-epimorphism-Set :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
    ({l : Level}  is-epimorphism-Set l f)  is-surjective f
  is-surjective-is-epimorphism-Set {l1} {l2} {A} {B} {f} H b =
      ( equiv-eq
        ( ap
          ( pr1)
          ( htpy-eq
            ( is-injective-is-emb
              ( H (Prop-Set (l1  l2)))
              { g}
              { h}
              ( eq-htpy
                ( λ a 
                    ( λ _  unit-trunc-Prop (pair a refl))
                    ( λ _  raise-star))))
            ( b))))
      ( raise-star)
    g : B  Prop (l1  l2)
    g y = raise-unit-Prop (l1  l2)
    h : B  Prop (l1  l2)
    h y = ∃-Prop A  x  f x  y)

Recent changes