This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Dependent epimorphisms

module foundation.dependent-epimorphisms where

Imports

open import foundation.epimorphisms
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.precomposition-dependent-functions

Idea

A dependent epimorphism is a map f : A → B such that the precomposition function

  - ∘ f : ((b : B) → C b) → ((a : A) → C (f a))

is an embedding for every type family C over B.

Clearly, every dependent epimorphism is an epimorphism. The converse is also true, i.e., every epimorphism is a dependent epimorphism. Therefore it follows that a map f : A → B is acyclic if and only if it is an epimorphism, if and only if it is a dependent epimorphism.

Definitions

The predicate of being a dependent epimorphism

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

  is-dependent-epimorphism : (A → B) → UUω
  is-dependent-epimorphism f =
    {l : Level} (C : B → UU l) → is-emb (precomp-Π f C)

Properties

Every dependent epimorphism is an epimorphism

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

  is-epimorphism-is-dependent-epimorphism :
    is-dependent-epimorphism f → is-epimorphism f
  is-epimorphism-is-dependent-epimorphism e X = e (λ _ → X)

The converse of the above, that every epimorphism is a dependent epimorphism, can be found in the file on acyclic maps.

agda-unimath