Require Import Category.Core Functor.Core HomFunctor Category.Morphisms Category.Dual Functor.Dual Category.Prod Functor.Prod NaturalTransformation.Core SetCategory.Core Functor.Composition.Core.
Require Import Basics.Trunc Types.Universe HIT.iso HoTT.Truncations.Core.

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

Local Open Scope category_scope.

Section full_faithful.
  Context `{Funext}.
  Variables C D : PreCategory.
  Variable F : Functor C D.

  Definition induced_hom_natural_transformation
  : NaturalTransformation (hom_functor C) (hom_functor D o (F^op, F)).
  Proof.
    refine (Build_NaturalTransformation
              (hom_functor C)
              (hom_functor D o (F^op, F))
              (fun (sd : object (C^op × C)) m ⇒ (F _1 m)%morphism)
              _
           ).
    abstract (
        repeat (intros [] || intro);
        simpl in *;
          repeat (apply path_forall; intro);
        simpl;
        rewrite !composition_of;
        reflexivity
      ).
  Defined.

  Class IsFull
    := is_full
       : ∀ x y : C,
           IsEpimorphism (induced_hom_natural_transformation (x, y)).

  Class IsFaithful
    := is_faithful
       : ∀ x y : C,
           IsMonomorphism (induced_hom_natural_transformation (x, y)).

  Class IsFullyFaithful
    := is_fully_faithful
       : ∀ x y : C,
           IsIsomorphism (induced_hom_natural_transformation (x, y)).

  Global Instance isfull_isfullyfaithful `{IsFullyFaithful}
  : IsFull.
  Proof.
    intros ? ?; hnf in × |- .
    typeclasses eauto.
  Qed.

  Global Instance isfaithful_isfullyfaithful `{IsFullyFaithful}
  : IsFaithful.
  Proof.
    intros ? ?; hnf in × |- .
    typeclasses eauto.
  Qed.

  Lemma isfullyfaithful_isfull_isfaithful_helper `{IsFull} `{IsFaithful}
        (H' : ∀ x y (m : morphism set_cat x y),
                IsEpimorphism m
                → IsMonomorphism m
                → IsIsomorphism m)
  : IsFullyFaithful.
  Proof.
    intros ? ?; hnf in × |- .
    apply H'; eauto.
  Qed.
End full_faithful.

Section fully_faithful_helpers.
  Context `{ua : Univalence}.
  Variables x y : HSet.
  Variable m : x → y.

  Lemma isisomorphism_isequiv_set_cat
        `{H' : IsEquiv _ _ m}
  : IsIsomorphism (m : morphism set_cat x y).
  Proof.
    ∃ (m^-1)%core;
    apply path_forall; intro;
    destruct H';
    simpl in *;
    eauto.
  Qed.

  Definition isequiv_isepimorphism_ismonomorphism
             (Hepi : IsEpimorphism (m : morphism set_cat x y))
             (Hmono : IsMonomorphism (m : morphism set_cat x y))
  : @IsEquiv _ _ m
    (* NB: This depends on the (arguably accidental) fact that `ismono` and `isepi` from HoTT core are *definitionally* identical to the specialization of `IsMonomorphism` and `IsEpimorphism` to the category of sets. *)
    := @isequiv_isepi_ismono _ x y m Hepi Hmono.
End fully_faithful_helpers.

Global Instance isfullyfaithful_isfull_isfaithful
       `{Univalence}
       `{Hfull : @IsFull _ C D F}
       `{Hfaithful : @IsFaithful _ C D F}
: @IsFullyFaithful _ C D F
  := fun x y ⇒ @isisomorphism_isequiv_set_cat
                  _ _ _ _
                  (@isequiv_isepimorphism_ismonomorphism
                     _ _ _ _
                     (Hfull x y)
                     (Hfaithful x y)).

Class IsSplitEssentiallySurjective A B (F : Functor A B)
  := is_split_essentially_surjective
     : ∀ b : B, ∃ a : A, F a <~=~> b.

Class IsEssentiallySurjective A B (F : Functor A B)
  := is_essentially_surjective
     : ∀ b : B, hexists (fun a : A ⇒ F a <~=~> b).

Class IsWeakEquivalence `{Funext} A B (F : Functor A B)
  := { is_fully_faithful__is_weak_equivalence : IsFullyFaithful F;
       is_essentially_surjective__is_weak_equivalence : IsEssentiallySurjective F }.
#[export] Existing Instances
  is_fully_faithful__is_weak_equivalence
  is_essentially_surjective__is_weak_equivalence.