Library CT.Instance.Functor.FullFunctor

Require Import CT.Category.
Require Import CT.Functor.

Full Functors

A "full" functor is one that is surjective on hom-sets. That is, A functor

$F : C \to D$ is full if

$\forall x, y \in C$ , the function

$F : C(x, y) \to D(F(x), F(y))$ is surjective.

So we require a Functor and a proof that surjectivity of hom-sets is satisfied.

Section FullFunctor.
  Context {A B : Category}.
  Variable (F : Functor A B).

  Definition FullFunctor :=
    ∀ {a b} (f : mor B (F_ob F a) (F_ob F b)),
      { f' : mor A a b | F_mor F f' = f }.
End FullFunctor.