Library UniMath.CategoryTheory.Subcategory.FullEquivalences

Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Subcategory.Core.
Require Import UniMath.CategoryTheory.Subcategory.Full.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.

Local Open Scope cat.

Equivalences between full subcategories
Section EquivalenceFullSub.
  Context {C₁ C₂ : category}
          {P : hsubtype C₁}
          {Q : hsubtype C₂}
          (L : C₁ ⟶ C₂)
          (L_equiv : adj_equivalence_of_cats L)
          (HL : ∏ (x : C₁), P x → Q (L x))
          (HR : ∏ (x : C₂), Q x → P (right_adjoint L_equiv x)).

  Let L' : full_sub_category C₁ P ⟶ full_sub_category C₂ Q
    := full_sub_category_functor P Q L HL.
  Let R' : full_sub_category C₂ Q ⟶ full_sub_category C₁ P
    := full_sub_category_functor Q P _ HR.

  Definition full_sub_category_equivalence_unit_data
    : nat_trans_data
        (functor_identity (full_sub_category C₁ P))
        (L' ∙ R')
    := λ y, unit_from_left_adjoint L_equiv (pr1 y) ,, tt.

  Definition full_sub_category_equivalence_unit_is_nat_trans
    : is_nat_trans
        _ _
        full_sub_category_equivalence_unit_data.
  Show proof.
    intros y₁ y₂ f ; cbn.
    use subtypePath.
    {
      intro.
      apply isapropunit.
    }
    cbn.
    apply (nat_trans_ax (unit_from_left_adjoint L_equiv)).

  Definition full_sub_category_equivalence_unit
    : functor_identity _ ⟹ L' ∙ R'.
  Show proof.
    use make_nat_trans.
    - exact full_sub_category_equivalence_unit_data.
    - exact full_sub_category_equivalence_unit_is_nat_trans.

  Definition full_sub_category_equivalence_counit_data
    : nat_trans_data
        (R' ∙ L')
        (functor_identity _)
    := λ y, counit_from_left_adjoint L_equiv (pr1 y) ,, tt.

  Definition full_sub_category_equivalence_counit_is_nat_trans
    : is_nat_trans
        _ _
        full_sub_category_equivalence_counit_data.
  Show proof.
    intros y₁ y₂ f ; cbn.
    use subtypePath.
    {
      intro.
      apply isapropunit.
    }
    cbn.
    apply (nat_trans_ax (counit_from_left_adjoint L_equiv)).

  Definition full_sub_category_equivalence_counit
    : R' ∙ L' ⟹ functor_identity _.
  Show proof.
    use make_nat_trans.
    - exact full_sub_category_equivalence_counit_data.
    - exact full_sub_category_equivalence_counit_is_nat_trans.

  Definition full_sub_category_equivalence
    : equivalence_of_cats
        (full_sub_category C₁ P)
        (full_sub_category C₂ Q).
  Show proof.
    use make_equivalence_of_cats.
    - use make_adjunction_data.
      + exact L'.
      + exact R'.
      + exact full_sub_category_equivalence_unit.
      + exact full_sub_category_equivalence_counit.
    - split.
      + intro.
        apply is_iso_full_sub.
        apply unit_nat_z_iso_from_adj_equivalence_of_cats.
      + intro.
        apply is_iso_full_sub.
        apply counit_nat_z_iso_from_adj_equivalence_of_cats.

  Definition full_sub_category_adj_equivalence
    : adj_equivalence_of_cats (full_sub_category_functor P Q L HL)
    := adjointification
         full_sub_category_equivalence.
End EquivalenceFullSub.