Library UniMath.Bicategories.RezkCompletions.RezkCompletionOfBicategory
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.YonedaLemma.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.
Require Import UniMath.Bicategories.RezkCompletions.BicatToLocalUnivalentBicat.
Require Import UniMath.CategoryTheory.rezk_completion.
Require Import UniMath.CategoryTheory.RezkCompletion.
Local Open Scope cat.
Section RezkCompletionBicategory.
Definition rezk_completion_2_1
(R : RezkCat) (B : bicat)
: ∑ RB : bicat,
∑ HB : psfunctor B RB,
is_univalent_2_1 RB × weak_biequivalence HB.
Show proof.
exists (LRB R B).
exists (psfunctor_B_to_LRB R B).
exists (LRB_is_locally_univalent R B).
exact (psfunctor_B_to_LRB_is_weak_biequivalence R B).
exists (psfunctor_B_to_LRB R B).
exists (LRB_is_locally_univalent R B).
exact (psfunctor_B_to_LRB_is_weak_biequivalence R B).
Definition rezk_completion_2 (R : RezkCat) (B : bicat)
: ∑ RB : bicat,
∑ HB : psfunctor B RB,
is_univalent_2 RB × weak_biequivalence HB.
Show proof.
set (r := rezk_completion_2_0 (LRB R B) (LRB_is_locally_univalent R B)).
exists (pr1 r).
exists (comp_psfunctor (pr12 r) (psfunctor_B_to_LRB R B)).
exists (pr122 r).
use comp_weak_biequivalence.
- apply psfunctor_B_to_LRB_is_weak_biequivalence.
- exact (weak_equivalence_to_is_weak_biequivalence _ (pr222 r)).
exists (pr1 r).
exists (comp_psfunctor (pr12 r) (psfunctor_B_to_LRB R B)).
exists (pr122 r).
use comp_weak_biequivalence.
- apply psfunctor_B_to_LRB_is_weak_biequivalence.
- exact (weak_equivalence_to_is_weak_biequivalence _ (pr222 r)).
End RezkCompletionBicategory.
Definition rezk_completion_2_presheaves
(B : bicat)
: ∑ RB : bicat,
∑ HB : psfunctor B RB,
is_univalent_2 RB × weak_biequivalence HB.
Show proof.
use rezk_completion_2.
exact (λ C, _ ,, _ ,, Rezk_eta_essentially_surjective C ,, Rezk_eta_fully_faithful C).
exact (λ C, _ ,, _ ,, Rezk_eta_essentially_surjective C ,, Rezk_eta_fully_faithful C).