Definition rezk_completion_2 (R : RezkCat) (B : bicat) : ∑ RB : bicat, ∑ HB : psfunctor B RB, is_univalent_2 RB × weak_biequivalence HB. 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)). Defined.
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.PseudoFunctors.Properties. Require Import UniMath.Bicategories.RezkCompletions.BicatToLocalUnivalentBicat. Require Import UniMath.CategoryTheory.RezkCompletions.Construction. Require Import UniMath.CategoryTheory.RezkCompletions.RezkCompletions.