# Faithful functors between precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-26.

module category-theory.faithful-functors-precategories where
Imports
open import category-theory.faithful-maps-precategories
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.embeddings
open import foundation.equivalences
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

## Idea

A functor between precategories C and D is faithful if it's an embedding on hom-sets.

Note that embeddings on sets happen to coincide with injections. However, we define faithful functors in terms of embeddings because this is the notion that generalizes.

## Definition

### The predicate on functors between precategories of being faithful

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

is-faithful-functor-Precategory : UU (l1  l2  l4)
is-faithful-functor-Precategory =
is-faithful-map-Precategory C D (map-functor-Precategory C D F)

is-prop-is-faithful-functor-Precategory :
is-prop is-faithful-functor-Precategory
is-prop-is-faithful-functor-Precategory =
is-prop-is-faithful-map-Precategory C D (map-functor-Precategory C D F)

is-faithful-prop-functor-Precategory : Prop (l1  l2  l4)
is-faithful-prop-functor-Precategory =
is-faithful-prop-map-Precategory C D (map-functor-Precategory C D F)

### The type of faithful functors between two precategories

faithful-functor-Precategory :
{l1 l2 l3 l4 : Level}
(C : Precategory l1 l2)
(D : Precategory l3 l4)  UU (l1  l2  l3  l4)
faithful-functor-Precategory C D =
Σ (functor-Precategory C D) (is-faithful-functor-Precategory C D)

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

functor-faithful-functor-Precategory : functor-Precategory C D
functor-faithful-functor-Precategory = pr1 F

is-faithful-faithful-functor-Precategory :
is-faithful-functor-Precategory C D functor-faithful-functor-Precategory
is-faithful-faithful-functor-Precategory = pr2 F

obj-faithful-functor-Precategory : obj-Precategory C  obj-Precategory D
obj-faithful-functor-Precategory =
obj-functor-Precategory C D functor-faithful-functor-Precategory

hom-faithful-functor-Precategory :
{x y : obj-Precategory C}
hom-Precategory C x y
hom-Precategory D
( obj-faithful-functor-Precategory x)
( obj-faithful-functor-Precategory y)
hom-faithful-functor-Precategory =
hom-functor-Precategory C D functor-faithful-functor-Precategory

### The predicate on functors between precategories of being injective on hom-sets

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

is-injective-hom-functor-Precategory : UU (l1  l2  l4)
is-injective-hom-functor-Precategory =
is-injective-hom-map-Precategory C D (map-functor-Precategory C D F)

is-prop-is-injective-hom-functor-Precategory :
is-prop is-injective-hom-functor-Precategory
is-prop-is-injective-hom-functor-Precategory =
is-prop-is-injective-hom-map-Precategory C D
( map-functor-Precategory C D F)

is-injective-hom-prop-functor-Precategory : Prop (l1  l2  l4)
is-injective-hom-prop-functor-Precategory =
is-injective-hom-prop-map-Precategory C D
( map-functor-Precategory C D F)

## Properties

### A functor of precategories is faithful if and only if it is injective on hom-sets

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

is-injective-hom-is-faithful-functor-Precategory :
is-faithful-functor-Precategory C D F
is-injective-hom-functor-Precategory C D F
is-injective-hom-is-faithful-functor-Precategory =
is-injective-hom-is-faithful-map-Precategory C D
( map-functor-Precategory C D F)

is-faithful-is-injective-hom-functor-Precategory :
is-injective-hom-functor-Precategory C D F
is-faithful-functor-Precategory C D F
is-faithful-is-injective-hom-functor-Precategory =
is-faithful-is-injective-hom-map-Precategory C D
( map-functor-Precategory C D F)

is-equiv-is-injective-hom-is-faithful-functor-Precategory :
is-equiv is-injective-hom-is-faithful-functor-Precategory
is-equiv-is-injective-hom-is-faithful-functor-Precategory =
is-equiv-is-injective-hom-is-faithful-map-Precategory C D
( map-functor-Precategory C D F)

is-equiv-is-faithful-is-injective-hom-functor-Precategory :
is-equiv is-faithful-is-injective-hom-functor-Precategory
is-equiv-is-faithful-is-injective-hom-functor-Precategory =
is-equiv-is-faithful-is-injective-hom-map-Precategory C D
( map-functor-Precategory C D F)

equiv-is-injective-hom-is-faithful-functor-Precategory :
is-faithful-functor-Precategory C D F
is-injective-hom-functor-Precategory C D F
equiv-is-injective-hom-is-faithful-functor-Precategory =
equiv-is-injective-hom-is-faithful-map-Precategory C D
( map-functor-Precategory C D F)

equiv-is-faithful-is-injective-hom-functor-Precategory :
is-injective-hom-functor-Precategory C D F
is-faithful-functor-Precategory C D F
equiv-is-faithful-is-injective-hom-functor-Precategory =
equiv-is-faithful-is-injective-hom-map-Precategory C D
( map-functor-Precategory C D F)

### Faithful functors are faithful on isomorphisms

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

is-faithful-on-isos-is-faithful-functor-Precategory :
(x y : obj-Precategory C)
is-emb (preserves-iso-functor-Precategory C D F {x} {y})
is-faithful-on-isos-is-faithful-functor-Precategory x y =
is-emb-right-factor _ _
( is-emb-inclusion-subtype (is-iso-prop-Precategory D))
( is-emb-comp _ _
( is-faithful-F x y)
( is-emb-inclusion-subtype (is-iso-prop-Precategory C)))