Library UniMath.CategoryTheory.WeakEquivalences.Core

The basics of weak equivalences
Contents. 1. Section ``WeakEquivalences'' contains:
  • the definition of a weak equivalence (i.e., essentially surjective and fully faithful);
  • together with accessors;
  • a proof that ``is a weak equivalence'' is a proposition;
  • a proof that every identity functor (resp. the composite of weak equivalences) is a weak equivalence
2. Section ``WeakEquivalenceInducesIsoOnUnivalentFunctorCategories'' contains a proof for the statement: Let H : C → D be a weak equivalence (between not-necesssarily univalent categories) and E a univalent category. Then, the functor (H · -) : D, E → C, E is an isomorphism of (univalent) categories; and hence an isomorphism.
3. Section ``WeakAndAdjointEquivalences'' contains relations between weak and adjoint equivalences

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.

Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.

Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.catiso.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.PrecompEquivalence.

Local Open Scope cat.

Section WeakEquivalences.

  Definition is_weak_equiv
    {C D : category} (H : functor C D) : UU
    := essentially_surjective H × fully_faithful H.

  Definition eso_from_weak_equiv
    {C D : category} (F : C ⟶ D)
    : is_weak_equiv F → essentially_surjective F
    := pr1.

  Definition ff_from_weak_equiv
    {C D : category} (F : C ⟶ D)
    : is_weak_equiv F → fully_faithful F
    := pr2.

  Lemma isaprop_is_weak_equiv
    {C D : category} (H : functor C D)
    : isaprop (is_weak_equiv H).
  Show proof.
    apply isapropdirprod.
    - apply isaprop_essentially_surjective.
    - apply isaprop_fully_faithful.

  Lemma id_is_weak_equiv
    (C : category)
    : is_weak_equiv (functor_identity C).
  Show proof.
    split.
    - apply identity_functor_is_essentially_surjective.
    - apply identity_functor_is_fully_faithful.

  Definition comp_is_weak_equiv
    {C D E : category}
    (H : C ⟶ D) (I : D ⟶ E)
    : is_weak_equiv H → is_weak_equiv I
      → is_weak_equiv (H ∙ I).
  Show proof.
    intros Hw Iw.
    split.
    - exact (comp_essentially_surjective
        _ (eso_from_weak_equiv _ Hw)
        _ (eso_from_weak_equiv _ Iw)).
    - exact (comp_ff_is_ff _ _ _
               _ (ff_from_weak_equiv _ Hw)
               _ (ff_from_weak_equiv _ Iw)).

  Definition weak_equiv
    (C D : category) : UU
    := ∑ H : C ⟶ D, is_weak_equiv H.

End WeakEquivalences.

Section WeakEquivalenceInducesIsoOnUnivalentFunctorCategories.

  Context {C D : category}
    (H : C ⟶ D)
    (Hw : is_weak_equiv H).

  Definition precomp_is_iso
    : ∏ E : univalent_category, is_catiso (pre_composition_functor _ _ E H).
  Show proof.
    intro E.
    transparent assert (a : (Core.adj_equivalence_of_cats (pre_composition_functor _ _ (pr1 E) H))). {
      apply precomp_adjoint_equivalence ; apply Hw.
    }

    use (pr2 (adj_equivalence_of_cats_to_cat_iso a _ _))
    ; apply is_univalent_functor_category ; apply E.

  Definition precomp_is_equality
    : ∏ E : univalent_category, [D, E] = [C, E].
  Show proof.
    intro E.
    apply catiso_to_category_path.
    exact (_ ,, precomp_is_iso E).

End WeakEquivalenceInducesIsoOnUnivalentFunctorCategories.

Section WeakAndAdjointEquivalences.

  Context {A B : category} {F : A ⟶ B}.

  Lemma rad_equivalence_of_cats''
    (A_univ : is_univalent A)
    (F_weq : is_weak_equiv F)
    : adj_equivalence_of_cats F.
  Show proof.
    apply rad_equivalence_of_cats.
    - exact A_univ.
    - apply F_weq.
    - apply F_weq.

  Lemma weak_equiv_from_equiv
    (Fe : adj_equivalence_of_cats F)
    : is_weak_equiv F.
  Show proof.
    split.
    - apply functor_from_equivalence_is_essentially_surjective, Fe.
    - apply fully_faithful_from_equivalence, Fe.

End WeakAndAdjointEquivalences.