(** * Attributes of Functoriality of functor composition *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Composition.Functorial.Core.
Require Import NaturalTransformation.Composition.Core.
Require Import NaturalTransformation.Isomorphisms.
Require Import Functor.Attributes.
Require Import FunctorCategory.Core.
Require Import Category.Morphisms.
Require Import NaturalTransformation.Paths.
Require Import HoTT.Truncations.Core.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope category_scope.
Local Open Scope natural_transformation_scope.
Local Open Scope morphism_scope.

(** ** Precomposition with an essentially surjective functor is faithful *)
Section faithfull_precomposition_essential_surjective.
  (** Quoting the HoTT Book:

  Lemma. If [A], [B], [C] are precategories and [H : A → B] is an
  essentially surjective functor, then [(– ∘ H) : (B → C) → (A → C)]
  is faithful. *)

  Context `{fs : Funext}.
  Variables A B C : PreCategory.

  Variable H : Functor A B.

  Context `{H_is_essentially_surjective : IsEssentiallySurjective A B H}.

  Lemma isfaithful_precomposition_essentially_surjective_helper
        (F G : Functor B C)
        (T U : NaturalTransformation F G)
        (a : A) (b : B)
        (f : H a <~=~> b)
        (H' : T oR H = U oR H)
  : T b = U b.
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
F, G: Functor B C
T, U: NaturalTransformation F G
a: A
b: B
f: H _0 a <~=~> b
H': T oR H = U oR H
T b = U b
  Proof.
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
F, G: Functor B C
T, U: NaturalTransformation F G
a: A
b: B
f: H _0 a <~=~> b
H': T oR H = U oR H
T b = U b
    apply (ap components_of) in H'.
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
F, G: Functor B C
T, U: NaturalTransformation F G
a: A
b: B
f: H _0 a <~=~> b
H': T oR H = U oR H
T b = U b
    apply apD10 in H'; hnf in H'; simpl in H'.
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
F, G: Functor B C
T, U: NaturalTransformation F G
a: A
b: B
f: H _0 a <~=~> b
H': forall x : A,
T (H _0 x)%object = U (H _0 x)%object
T b = U b
    rewrite <- !(path_components_of_isomorphic' f).
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
F, G: Functor B C
T, U: NaturalTransformation F G
a: A
b: B
f: H _0 a <~=~> b
H': forall x : A,
T (H _0 x)%object = U (H _0 x)%object
G _1 f o T (H _0 a)%object o (F _1 f)^-1 =
G _1 f o U (H _0 a)%object o (F _1 f)^-1
    rewrite H'.
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
F, G: Functor B C
T, U: NaturalTransformation F G
a: A
b: B
f: H _0 a <~=~> b
H': forall x : A,
T (H _0 x)%object = U (H _0 x)%object
G _1 f o U (H _0 a)%object o (F _1 f)^-1 =
G _1 f o U (H _0 a)%object o (F _1 f)^-1
    reflexivity.
  Qed.

  #[export] Instance isfaithful_precomposition_essentially_surjective
  : @IsFaithful _ (B -> C) (A -> C) (compose_functor _ _ _ H).
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
IsFaithful ((compose_functor A B C) _0 H)%object
  Proof.
fs: Funext
A, B, C: PreCategory
H: Functor A B
H_is_essentially_surjective: IsEssentiallySurjective
  H
IsFaithful ((compose_functor A B C) _0 H)%object
    repeat match goal with
             | _ => eapply isfaithful_precomposition_essentially_surjective_helper;
                   eassumption
             | _ => intro
             | _ => progress hnf in *
             | _ => progress simpl in *
             | _ => apply path_forall
             | _ => progress strip_truncations
             | [ H : _ |- _ ] => apply ap10 in H
             | _ => progress path_natural_transformation
             | [ H : sig _ |- _ ] => destruct H
             | [ H : _, t : _ |- _ ]
               => generalize dependent (H t); clear H
           end.
  Qed.
End faithfull_precomposition_essential_surjective.