Library UniMath.CategoryTheory.RezkCompletions.Construction

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Propositions.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.yoneda.
Require Import UniMath.CategoryTheory.Subcategory.Core.
Require Import UniMath.CategoryTheory.Subcategory.Full.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.whiskering.

Require Export UniMath.CategoryTheory.RezkCompletions.RezkCompletions.

Local Open Scope cat.

2. The construction of the Rezk completion and the embedding F

Section RezkCompletion.

  Context (A : category).

  Definition Rezk_completion_category : category.
  Show proof.

exists (full_img_sub_precategory (yoneda A)).
exact (has_homsets_full_img_sub_precategory (yoneda A)).

Definition Rezk_completion_univalent_category : univalent_category.
Show proof.

    exists Rezk_completion_category.
    apply is_univalent_full_sub_category.
    apply (is_univalent_functor_category _ _ is_univalent_HSET).

Definition Rezk_eta : functor A Rezk_completion_univalent_category.
Show proof.

apply (functor_full_img (yoneda A)).

Lemma Rezk_eta_fully_faithful : fully_faithful Rezk_eta.
Show proof.

apply (functor_full_img_fully_faithful_if_fun_is _ _ (yoneda A)).
apply yoneda_fully_faithful.

Lemma Rezk_eta_essentially_surjective : essentially_surjective Rezk_eta.
Show proof.

apply (functor_full_img_essentially_surjective _ _ (yoneda A)).

  Definition Rezk_completion
    : rezk_completion A.
  Show proof.

    use make_rezk_completion.
    - exact Rezk_completion_univalent_category.
    - exact Rezk_eta.
    - exact Rezk_eta_essentially_surjective.
    - exact Rezk_eta_fully_faithful.

  Section UniversalProperty.

    Context (C : category).
    Context (Ccat : is_univalent C).

    Definition Rezk_eta_adj_equiv
      : adj_equivalence_of_cats (pre_composition_functor A Rezk_completion C Rezk_eta)
      := rezk_completion_functor_equivalence _ Rezk_completion _ Ccat.

    Definition Rezk_eta_Universal_Property
      : isweq (pre_composition_functor _ _ C Rezk_eta)
      := rezk_completion_universal_property _ Rezk_completion _ Ccat.

    Definition Rezk_eta_weq
      : [Rezk_completion , C ] ≃ [A , C ]
      := make_weq _ Rezk_eta_Universal_Property.

    Definition Rezk_op_adj_equiv
      : adj_equivalence_of_cats
        (pre_composition_functor A ^op Rezk_completion ^op C
            (functor_opp Rezk_eta))
      := rezk_completion_opp_functor_equivalence A Rezk_completion _ Ccat.

    Definition Rezk_op_Universal_Property
      : isweq (pre_composition_functor A ^op Rezk_completion ^op C (functor_opp Rezk_eta))
      := rezk_completion_opp_universal_property _ Rezk_completion _ Ccat.

    Definition Rezk_opp_weq
      : [Rezk_completion ^op , C ] ≃ [A ^op , C ]
      := make_weq _ Rezk_op_Universal_Property.

  End UniversalProperty.

End RezkCompletion.