Library UniMath.CategoryTheory.rezk_completion
**********************************************************
Benedikt Ahrens, Chris Kapulkin, Mike Shulman
january 2013
**********************************************************
Contents : Rezk completion
- Construction of the Rezk completion via Yoneda
- Universal property of the Rezk completion
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Local Open Scope cat.
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 Import UniMath.CategoryTheory.precomp_fully_faithful.
Require Import UniMath.CategoryTheory.precomp_ess_surj.
Section rezk.
Context (A : category).
Definition category_Rezk_completion : category.
Show proof.
exists (full_img_sub_precategory (yoneda A)).
exact (has_homsets_full_img_sub_precategory (yoneda A)).
exact (has_homsets_full_img_sub_precategory (yoneda A)).
Definition Rezk_completion : univalent_category.
Show proof.
exists category_Rezk_completion.
apply is_univalent_full_sub_category.
apply (is_univalent_functor_category _ _ is_univalent_HSET).
apply is_univalent_full_sub_category.
apply (is_univalent_functor_category _ _ is_univalent_HSET).
Definition Rezk_eta : functor A Rezk_completion.
Show proof.
Lemma Rezk_eta_fully_faithful : fully_faithful Rezk_eta.
Show proof.
Lemma Rezk_eta_essentially_surjective : essentially_surjective Rezk_eta.
Show proof.
End rezk.
Definition functor_from (C : precategory) : UU
:= ∑ D : univalent_category, functor C D.
Coercion target_category (C : precategory) (X : functor_from C) : univalent_category := pr1 X.
Definition func_functor_from {C : precategory} (X : functor_from C) : functor C X := pr2 X.
Definition is_initial_functor_from (C : precategory) (X : functor_from C) : UU
:= ∏ X' : functor_from C,
∃! H : functor X X',
functor_composite (func_functor_from X) H = func_functor_from X'.
Section rezk_universal_property.
Context (A : category).
Section fix_a_category.
Context (C : category) (Ccat : is_univalent C).
Lemma pre_comp_rezk_eta_is_fully_faithful :
fully_faithful
(pre_composition_functor _ _ C (Rezk_eta A)).
Show proof.
apply pre_composition_with_ess_surj_and_fully_faithful_is_fully_faithful.
- apply Rezk_eta_essentially_surjective.
- apply Rezk_eta_fully_faithful.
- apply Rezk_eta_essentially_surjective.
- apply Rezk_eta_fully_faithful.
Lemma pre_comp_rezk_eta_is_ess_surj :
essentially_surjective (pre_composition_functor _ _ C (Rezk_eta A)).
Show proof.
apply pre_composition_essentially_surjective.
- apply Ccat.
- apply Rezk_eta_essentially_surjective.
- apply Rezk_eta_fully_faithful.
- apply Ccat.
- apply Rezk_eta_essentially_surjective.
- apply Rezk_eta_fully_faithful.
Definition Rezk_adj_equiv : adj_equivalence_of_cats
(pre_composition_functor _ _ C (Rezk_eta A)).
Show proof.
apply (@rad_equivalence_of_cats
(functor_category (Rezk_completion A) C)
(functor_category A C)
(is_univalent_functor_category _ _ Ccat )
_
(pre_comp_rezk_eta_is_fully_faithful)
(pre_comp_rezk_eta_is_ess_surj)).
(functor_category (Rezk_completion A) C)
(functor_category A C)
(is_univalent_functor_category _ _ Ccat )
_
(pre_comp_rezk_eta_is_fully_faithful)
(pre_comp_rezk_eta_is_ess_surj)).
Theorem Rezk_eta_Universal_Property :
isweq (pre_composition_functor _ _ C (Rezk_eta A)).
Show proof.
apply adj_equiv_of_cats_is_weq_of_objects.
- apply is_univalent_functor_category;
assumption.
- apply is_univalent_functor_category;
assumption.
- apply Rezk_adj_equiv.
- apply is_univalent_functor_category;
assumption.
- apply is_univalent_functor_category;
assumption.
- apply Rezk_adj_equiv.
Definition Rezk_weq : [Rezk_completion A, C] ≃ [A, C ]
:= make_weq _ Rezk_eta_Universal_Property.
End fix_a_category.
Lemma Rezk_initial_functor_from : is_initial_functor_from A
(tpair _ (Rezk_completion A) (Rezk_eta A)).
Show proof.
Definition Rezk_completion_endo_is_identity (D : functor_from A)
(DH : is_initial_functor_from A D)
: ∏ X : functor D D, functor_composite (func_functor_from D) X = func_functor_from D
->
X = functor_identity D.
Show proof.
intros X H.
set (DH' := DH D).
intermediate_path (pr1 (pr1 DH')).
- apply path_to_ctr.
apply H.
- apply pathsinv0.
apply path_to_ctr.
apply functor_identity_right.
set (DH' := DH D).
intermediate_path (pr1 (pr1 DH')).
- apply path_to_ctr.
apply H.
- apply pathsinv0.
apply path_to_ctr.
apply functor_identity_right.
End rezk_universal_property.
Section opp_rezk_universal_property.
Context (A : category).
Section fix_a_category.
Context (C : category) (Ccat : is_univalent C).
Lemma pre_comp_rezk_eta_opp_is_fully_faithful :
fully_faithful
(pre_composition_functor A^op (Rezk_completion A)^op C
(functor_opp (Rezk_eta A))).
Show proof.
apply pre_composition_with_ess_surj_and_fully_faithful_is_fully_faithful.
- apply opp_functor_essentially_surjective.
apply Rezk_eta_essentially_surjective.
- apply opp_functor_fully_faithful.
apply Rezk_eta_fully_faithful.
- apply opp_functor_essentially_surjective.
apply Rezk_eta_essentially_surjective.
- apply opp_functor_fully_faithful.
apply Rezk_eta_fully_faithful.
Lemma pre_comp_rezk_eta_opp_is_ess_surj :
essentially_surjective
(pre_composition_functor A^op (Rezk_completion A)^op C
(functor_opp (Rezk_eta A))).
Show proof.
apply pre_composition_essentially_surjective.
- apply Ccat.
- apply opp_functor_essentially_surjective.
apply Rezk_eta_essentially_surjective.
- apply opp_functor_fully_faithful.
apply Rezk_eta_fully_faithful.
- apply Ccat.
- apply opp_functor_essentially_surjective.
apply Rezk_eta_essentially_surjective.
- apply opp_functor_fully_faithful.
apply Rezk_eta_fully_faithful.
Definition Rezk_op_adj_equiv :
adj_equivalence_of_cats
(pre_composition_functor A^op (Rezk_completion A)^op C
(functor_opp (Rezk_eta A))).
Show proof.
apply (@rad_equivalence_of_cats
[(Rezk_completion A)^op, C]
[A^op, C]
(is_univalent_functor_category _ _ Ccat )
_
(pre_comp_rezk_eta_opp_is_fully_faithful)
(pre_comp_rezk_eta_opp_is_ess_surj)).
[(Rezk_completion A)^op, C]
[A^op, C]
(is_univalent_functor_category _ _ Ccat )
_
(pre_comp_rezk_eta_opp_is_fully_faithful)
(pre_comp_rezk_eta_opp_is_ess_surj)).
Theorem Rezk_eta_opp_Universal_Property :
isweq (pre_composition_functor A^op (Rezk_completion A)^op C
(functor_opp (Rezk_eta A))).
Show proof.
apply adj_equiv_of_cats_is_weq_of_objects.
- apply is_univalent_functor_category;
assumption.
- apply is_univalent_functor_category;
assumption.
- apply Rezk_op_adj_equiv.
- apply is_univalent_functor_category;
assumption.
- apply is_univalent_functor_category;
assumption.
- apply Rezk_op_adj_equiv.
Definition Rezk_opp_weq : [(Rezk_completion A)^op, C] ≃ [A^op, C]
:= make_weq _ Rezk_eta_opp_Universal_Property.
End fix_a_category.
End opp_rezk_universal_property.