# Essentially surjective functors between precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-01.

module category-theory.essentially-surjective-functors-precategories where

Imports
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.propositions
open import foundation.universe-levels


## Idea

A functor F : C → D between precategories is essentially surjective if there for every object y : D merely exists an object x : C such that F x ≅ y.

## Definitions

### The predicate of being essentially surjective

module _
{l1 l2 l3 l4 : Level}
(C : Precategory l1 l2) (D : Precategory l3 l4)
(F : functor-Precategory C D)
where

is-essentially-surjective-prop-functor-Precategory : Prop (l1 ⊔ l3 ⊔ l4)
is-essentially-surjective-prop-functor-Precategory =
Π-Prop
( obj-Precategory D)
( λ y →
exists-structure-Prop
( obj-Precategory C)
( λ x → iso-Precategory D (obj-functor-Precategory C D F x) y))

is-essentially-surjective-functor-Precategory : UU (l1 ⊔ l3 ⊔ l4)
is-essentially-surjective-functor-Precategory =
( y : obj-Precategory D) →
exists-structure
( obj-Precategory C)
( λ x → iso-Precategory D (obj-functor-Precategory C D F x) y)

is-prop-is-essentially-surjective-functor-Precategory :
is-prop is-essentially-surjective-functor-Precategory
is-prop-is-essentially-surjective-functor-Precategory =
is-prop-type-Prop is-essentially-surjective-prop-functor-Precategory


### The type of essentially surjective functors

essentially-surjective-functor-Precategory :
{l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) →
UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
essentially-surjective-functor-Precategory C D =
Σ ( functor-Precategory C D)
( is-essentially-surjective-functor-Precategory C D)

module _
{l1 l2 l3 l4 : Level}
(C : Precategory l1 l2) (D : Precategory l3 l4)
(F : essentially-surjective-functor-Precategory C D)
where

functor-essentially-surjective-functor-Precategory :
functor-Precategory C D
functor-essentially-surjective-functor-Precategory = pr1 F

is-essentially-surjective-essentially-surjective-functor-Precategory :
is-essentially-surjective-functor-Precategory C D
( functor-essentially-surjective-functor-Precategory)
is-essentially-surjective-essentially-surjective-functor-Precategory = pr2 F

obj-essentially-surjective-functor-Precategory :
obj-Precategory C → obj-Precategory D
obj-essentially-surjective-functor-Precategory =
obj-functor-Precategory C D
( functor-essentially-surjective-functor-Precategory)

hom-essentially-surjective-functor-Precategory :
{x y : obj-Precategory C} →
hom-Precategory C x y →
hom-Precategory D
( obj-essentially-surjective-functor-Precategory x)
( obj-essentially-surjective-functor-Precategory y)
hom-essentially-surjective-functor-Precategory =
hom-functor-Precategory C D
( functor-essentially-surjective-functor-Precategory)


## Properties

### Precomposing by essentially surjective functors define fully faithful functors

This remains to be shown. This is Lemma 8.2 of Univalent Categories and the Rezk completion.