open import Cat.Prelude

module Cat.Functor.Base where


# Functors🔗

This module defines the most important clases of functors: Full, faithful, fully faithful (abbreviated ff), split essentially surjective and (“merely”) essentially surjective.

A functor is full when its action on hom-sets is surjective:

is-full : Functor C D → Type _
is-full {C = C} {D = D} F =
∀ {x y} (g : D .Hom (F₀ F x) (F₀ F y)) → ∃[ f ∈ C .Hom x y ] (F₁ F f ≡ g)


A functor is faithful when its action on hom-sets is injective:

is-faithful : Functor C D → Type _
is-faithful F = ∀ {x y} → injective (F₁ F {x = x} {y})


## ff Functors🔗

A functor is fully faithful (abbreviated ff) when its action on hom-sets is an equivalence. Since Hom-sets are sets, it suffices for the functor to be full and faithful; Rather than taking this conjunction as a definition, we use the more directly useful data as a definition and prove the conjunction as a theorem.

is-fully-faithful : Functor C D → Type _
is-fully-faithful F = ∀ {x y} → is-equiv (F₁ F {x = x} {y})

fully-faithful→faithful : {F : Functor C D} → is-fully-faithful F → is-faithful F
fully-faithful→faithful {F = F} ff {_} {_} {x} {y} p =
x                         ≡⟨ sym (equiv→unit ff x) ⟩≡
equiv→inverse ff (F₁ F x) ≡⟨ ap (equiv→inverse ff) p ⟩≡
equiv→inverse ff (F₁ F y) ≡⟨ equiv→unit ff y ⟩≡
y                         ∎

full+faithful→ff
: (F : Functor C D) → is-full F → is-faithful F → is-fully-faithful F
full+faithful→ff {C = C} {D = D} F surj inj .is-eqv = p where
img-is-prop : ∀ {x y} f → is-prop (fibre (F₁ F {x = x} {y}) f)
img-is-prop f (g , p) (h , q) = Σ-prop-path (λ _ → D .Hom-set _ _ _ _) (inj (p ∙ sym q))

p : ∀ {x y} f → is-contr (fibre (F₁ F {x = x} {y}) f)
p f .centre = ∥-∥-elim (λ _ → img-is-prop f) (λ x → x) (surj f)
p f .paths = img-is-prop f _


A very important property of fully faithful functors (like $F$) is that they are conservative: If the image of $f : x \to y$ under $F$ is an isomorphism $Fx \cong Fy$, then $f$ was really an isomorphism $f : x \cong y$.

module _ {C : Precategory o h} {D : Precategory o₁ h₁} where
private
module C = Precategory C
module D = Precategory D

import Cat.Morphism C as Cm
import Cat.Morphism D as Dm

is-ff→is-conservative
: {F : Functor C D} → is-fully-faithful F
→ ∀ {X Y} (f : C.Hom X Y) → Dm.is-invertible (F₁ F f)
→ Cm.is-invertible f
is-ff→is-conservative {F = F} ff f isinv = i where
open Cm.is-invertible
open Cm.Inverses


Since the functor is ff, we can find a map “$F_1^{-1}(f) : y \to x$” in the domain category to serve as an inverse for $f$:

    g : C.Hom _ _
g = equiv→inverse ff (isinv .Dm.is-invertible.inv)
module ff {a} {b} = Equiv (_ , ff {a} {b})

Ffog =
F₁ F (f C.∘ g)    ≡⟨ F-∘ F _ _ ⟩≡
F₁ F f D.∘ F₁ F g ≡⟨ ap₂ D._∘_ refl (ff.ε _) ∙ isinv .Dm.is-invertible.invl ⟩≡
D.id              ∎

Fgof =
F₁ F (g C.∘ f)    ≡⟨ F-∘ F _ _ ⟩≡
F₁ F g D.∘ F₁ F f ≡⟨ ap₂ D._∘_ (ff.ε _) refl ∙ isinv .Dm.is-invertible.invr ⟩≡
D.id              ∎

i : Cm.is-invertible _
i .inv = g
i .inverses .invl =
f C.∘ g                    ≡⟨ sym (ff.η _) ⟩≡
ff.from ⌜ F₁ F (f C.∘ g) ⌝ ≡⟨ ap! (Ffog ∙ sym (F-id F)) ⟩≡
ff.from (F₁ F C.id)        ≡⟨ ff.η _ ⟩≡
C.id                       ∎
i .inverses .invr =
g C.∘ f                    ≡⟨ sym (ff.η _) ⟩≡
ff.from ⌜ F₁ F (g C.∘ f) ⌝ ≡⟨ ap! (Fgof ∙ sym (F-id F)) ⟩≡
ff.from (F₁ F C.id)        ≡⟨ ff.η _ ⟩≡
C.id                       ∎

is-ff→essentially-injective
: {F : Functor C D} → is-fully-faithful F
→ ∀ {X Y} → F₀ F X Dm.≅ F₀ F Y
→ X Cm.≅ Y
is-ff→essentially-injective {F = F} ff im = im′ where
-- Cm.make-iso (equiv→inverse ff to) inv invl invr
open Dm._≅_ im using (to ; from ; inverses)
D-inv′ : Dm.is-invertible (F₁ F (equiv→inverse ff to))
D-inv′ .Dm.is-invertible.inv = from
D-inv′ .Dm.is-invertible.inverses =
subst (λ e → Dm.Inverses e from) (sym (equiv→counit ff _)) inverses

open Cm.is-invertible (is-ff→is-conservative {F = F} ff (equiv→inverse ff to) D-inv′)

im′ : _ Cm.≅ _
im′ .to   = equiv→inverse ff to
im′ .from = inv
im′ .inverses .Cm.Inverses.invl = invl
im′ .inverses .Cm.Inverses.invr = invr


## Essential Fibres🔗

The essential fibre of a functor $F : C \to D$ over an object $y : D$ is the space of objects of $C$ which $F$ takes, up to isomorphism, to $y$.

Essential-fibre : Functor C D → D .Ob → Type _
Essential-fibre {D = D} F y = Σ[ x ∈ _ ] (F₀ F x ≅ y)
where open import Cat.Morphism D


A functor is split essentially surjective (abbreviated split eso) if there is a procedure for finding points in the essential fibre over any object. It’s essentially surjective if the this procedure merely, i.e. truncatedly, finds a point:

is-split-eso : Functor C D → Type _
is-split-eso F = ∀ y → Essential-fibre F y

is-eso : Functor C D → Type _
is-eso F = ∀ y → ∥ Essential-fibre F y ∥