# Fully faithful functors and equivalences

Authors: Benedikt Ahrens, Chris Kapulkin, Mike Shulman (January 2013) Revised by: Marco Maggesi (November 2017), Langston Barrett (April 2018)

## Contents :

• Fully faithful functor from an equivalence
• Functor from an equivalence is essentially surjective
• Fully faithful essentially surjective functors preserve all hProps on hom-types

## Fully faithful functor from an equivalence

Section from_equiv_to_fully_faithful.

Variables A B : precategory.
Variable F : A B.

Local Definition G : B A := adj_equivalence_inv H.

Local Definition eta : a : A, iso a (G (F a))

Local Definition eps : b : B, iso (F (G b)) b

Definition inverse {a b} (g : BF a, F b) : Aa, b
:= eta a · #G g · inv_from_iso (eta b).

Lemma inverse_is_inverse_1 a b (f : a --> b) : inverse (#F f) = f.
Proof.
unfold inverse.
set (H' := nat_trans_ax (adjunit (pr1 H))).
simpl in H'; rewrite <- H'; clear H'; simpl in ×.
rewrite <- assoc.
intermediate_path (f · identity _).
apply maponpaths.
set (H' := iso_inv_after_iso (eta b)).
apply H'.
rewrite id_right.
apply idpath.
Qed.

Lemma triangle_id_inverse (a : A)
: iso_inv_from_iso (functor_on_iso F (eta a)) = eps (F a).
Proof.
apply eq_iso. simpl.
match goal with | [ |- ?x = ?y ] ⇒ transitivity (x · identity _) end.
apply pathsinv0, id_right.
apply iso_inv_on_right.
set (H' := triangle_id_left_ad (pr2 (pr1 H)) a).
apply pathsinv0.
apply H'.
Qed.

Lemma triangle_id_inverse' (a : A)
: inv_from_iso (functor_on_iso F (eta a)) = eps (F a).
Proof.
apply (base_paths _ _ (triangle_id_inverse a)).
Qed.

Lemma inverse_is_inverse_2 a b (g : F a --> F b) : #F (inverse g) = g.
Proof.
unfold inverse.
repeat rewrite functor_comp.
rewrite functor_on_inv_from_iso.
simpl.
rewrite triangle_id_inverse'.
rewrite <- assoc.
set (H' := nat_trans_ax (adjcounit (pr1 H))).
simpl in H'; rewrite H'; clear H'.
rewrite assoc.
set (H' := pathsinv0 (triangle_id_left_ad (pr2 (pr1 H)) a)).
match goal with [|- ?f · ?g = ?h] ⇒ assert (H'' : identity _ = f) end.
- simpl in *; apply H'.
- rewrite <- H''. rewrite id_left. apply idpath.
Qed.

Lemma fully_faithful_from_equivalence : fully_faithful F.
Proof.
unfold fully_faithful. intros a b.
apply (isweq_iso _ (@inverse a b)).
- apply inverse_is_inverse_1.
- apply inverse_is_inverse_2.
Qed.

## Fully faithful essentially surjective functors preserve all hProps on hom-types

Section HomtypeProperties.

Context {C D : precategory} (F : functor C D).

For every hom-type in D, there merely exists a hom-type in C to which it is equivalent. For split essentially surjective functors, this could be strengthened to an untruncated version.
Lemma ff_es_homtype_weq (FFF : fully_faithful F) (FES : essentially_surjective F) :
( d d' : ob D, c c' : ob C, Cc, c' Dd, d' ).
Proof.
intros d d'.

Obtain the c, c' for which F c ≅ d and F c' ≅ d'.
apply (squash_to_prop (FES d)); [apply isapropishinh|]; intros c.
apply (squash_to_prop (FES d')); [apply isapropishinh|]; intros c'.
apply hinhpr.
(pr1 c), (pr1 c').

Homsets between isomorphic objects are equivalent.
intermediate_weq (D F (pr1 c), F (pr1 c') ).
- apply weq_from_fully_faithful; assumption.
- intermediate_weq (D F (pr1 c), d' ).
+ eapply make_weq.
apply iso_comp_left_isweq.
Unshelve.
exact (pr2 c').
+ eapply make_weq.
apply iso_comp_right_weq.
Unshelve.
exact (iso_inv_from_is_iso (pr1 (pr2 c)) (pr2 (pr2 c))).
Defined.

Lemma ff_es_homtype_property (FFF : fully_faithful F)
(FES : essentially_surjective F) (P : UU hProp)
(prop : a b : ob C, P (Ca, b)) : ( a b : ob D, P (Da, b)).
Proof.
intros a b.
apply (squash_to_prop (ff_es_homtype_weq FFF FES a b));
[apply propproperty|]; intros H.
use transportf.
- exact (P (C⟦(pr1 H), (pr1 (pr2 H))⟧)).
- apply maponpaths.
apply weqtopaths.
exact (pr2 (pr2 H)).
- apply prop.
Defined.

Corollary: Equivalences preserve hProps on hom-types.
Corollary equivalence_homtype_property (E : adj_equivalence_of_precats F)
(P : UU hProp) (prop : a b : ob C, P (Ca, b)) :
( a b : ob D, P (Da, b)).
Proof.
apply ff_es_homtype_property.
- apply fully_faithful_from_equivalence; assumption.
- apply functor_from_equivalence_is_essentially_surjective; assumption.
- assumption.
Defined.

Corollary: Fully faithful essentially surjective functors preserve the property of having hom-sets.
Corollary ff_es_preserves_homsets (FFF : fully_faithful F)
(FES : essentially_surjective F) (hsC : has_homsets C) : has_homsets D.
Proof.
refine (ff_es_homtype_property FFF FES
(λ t, make_hProp _ (isapropisaset t)) _).
apply hsC.
Defined.

Other applications: ff/es functors preserve univalence, being a groupoid, merely having any type of (co)limits, etc.