(* ******************************************************************************* *) (** * Yoneda Lemma Niccolo Veltri, Niels van der Weide June 2019 ********************************************************************************* *) Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Properties. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Properties. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.Yoneda. Require Import UniMath.Bicategories.PseudoFunctors.Representable. Require Import UniMath.Bicategories.Core.Examples.Image. Require Import UniMath.Bicategories.PseudoFunctors.Examples.CorestrictImage. Local Open Scope bicategory_scope. Local Open Scope cat. Opaque psfunctor. Section YonedaLemma. Context {B : bicat}. Variable (B_is_univalent_2_1 : is_univalent_2_1 B) (F : psfunctor (op1_bicat B) bicat_of_univ_cats) (X : B). (** First, we construct a functor from the yoneda to the presheaf *) Definition yoneda_to_presheaf_data_ob : pstrans (representable B_is_univalent_2_1 X) F → pr1 (F X). Proof. intro τ. pose (τ X) as f; cbn in f. exact (f (identity X)). Defined. Definition yoneda_to_presheaf_data_mor (η₁ η₂ : pstrans (representable B_is_univalent_2_1 X) F) (m : modification η₁ η₂) : yoneda_to_presheaf_data_ob η₁ --> yoneda_to_presheaf_data_ob η₂. Proof. pose (m X) as n; cbn in n. exact (n (identity X)). Defined. Definition yoneda_to_presheaf_data : functor_data (univ_hom (psfunctor_bicat_is_univalent_2_1 (op1_bicat B) bicat_of_univ_cats univalent_cat_is_univalent_2_1) (y B_is_univalent_2_1 X) F) (F X : univalent_category). Proof. use make_functor_data. - exact yoneda_to_presheaf_data_ob. - exact yoneda_to_presheaf_data_mor. Defined. Lemma yoneda_to_presheaf_is_functor : is_functor yoneda_to_presheaf_data. Proof. split. - intro η ; cbn. apply idpath. - intros η₁ η₂ η₃ f g ; cbn. apply idpath. Qed. Definition yoneda_to_presheaf : bicat_of_univ_cats ⟦ univ_hom (psfunctor_bicat_is_univalent_2_1 _ _ univalent_cat_is_univalent_2_1) (y B_is_univalent_2_1 X) F , F X ⟧. Proof. use make_functor. - exact yoneda_to_presheaf_data. - exact yoneda_to_presheaf_is_functor. Defined. (** Next, we construct a functor in the opposite direction *) Section PresheafToYonedaOb. Variable (x : (F X : univalent_category)). Definition presheaf_to_yoneda_ob_pstrans_functor_ob (Y : op1_bicat B) : B ⟦ Y , X ⟧ → pr1 (F Y) := λ f, (#F f : _ ⟶ _) x. Definition presheaf_to_yoneda_ob_pstrans_functor_mor (Y : op1_bicat B) (f g : B ⟦ Y , X ⟧) (α : f ==> g) : (presheaf_to_yoneda_ob_pstrans_functor_ob Y f) --> presheaf_to_yoneda_ob_pstrans_functor_ob Y g := (##F α : nat_trans _ _) x. Definition presheaf_to_yoneda_ob_pstrans_functor_data (Y : op1_bicat B) : functor_data (@hom B Y X) (pr1 (F Y)). Proof. use make_functor_data. - exact (presheaf_to_yoneda_ob_pstrans_functor_ob Y). - exact (presheaf_to_yoneda_ob_pstrans_functor_mor Y). Defined. Lemma presheaf_to_yoneda_ob_pstrans_is_functor (Y : op1_bicat B) : is_functor (presheaf_to_yoneda_ob_pstrans_functor_data Y). Proof. split. - intro f ; cbn. unfold presheaf_to_yoneda_ob_pstrans_functor_mor ; unfold presheaf_to_yoneda_ob_pstrans_functor_ob. exact (nat_trans_eq_pointwise (psfunctor_id2 F f) x). - intros f₁ f₂ f₃ α₁ α₂ ; cbn. unfold presheaf_to_yoneda_ob_pstrans_functor_mor. exact (nat_trans_eq_pointwise (psfunctor_vcomp F α₁ α₂) x). Qed. Definition presheaf_to_yoneda_ob_pstrans_functor (Y : op1_bicat B) : bicat_of_univ_cats ⟦ @univ_hom B B_is_univalent_2_1 Y X , F Y ⟧. Proof. use make_functor. - exact (presheaf_to_yoneda_ob_pstrans_functor_data Y). - exact (presheaf_to_yoneda_ob_pstrans_is_functor Y). Defined. Definition presheaf_to_yoneda_ob_pstrans_nat_trans_data (Y₁ Y₂ : op1_bicat B) (f : B ⟦ Y₂ , Y₁ ⟧) : nat_trans_data (presheaf_to_yoneda_ob_pstrans_functor Y₁ · # F f : _ ⟶ _) (#(y B_is_univalent_2_1 X : psfunctor _ _) f · presheaf_to_yoneda_ob_pstrans_functor Y₂ : _ ⟶ _). Proof. intros g ; cbn in *. unfold presheaf_to_yoneda_ob_pstrans_functor_ob. pose (psfunctor_comp F g f : _ ==> _) as p ; cbn in p. exact (p x). Defined. Lemma presheaf_to_yoneda_ob_pstrans_is_nat_trans (Y₁ Y₂ : op1_bicat B) (f : B ⟦ Y₂ , Y₁ ⟧) : is_nat_trans _ _ (presheaf_to_yoneda_ob_pstrans_nat_trans_data Y₁ Y₂ f). Proof. intros g₁ g₂ α ; cbn in *. unfold presheaf_to_yoneda_ob_pstrans_functor_mor ; unfold presheaf_to_yoneda_ob_pstrans_nat_trans_data. pose (psfunctor_rwhisker F f α) as p. pose (nat_trans_eq_pointwise p x) as q. exact (!q). Qed. Definition presheaf_to_yoneda_ob_pstrans_nat_trans (Y₁ Y₂ : op1_bicat B) (f : B ⟦ Y₂ , Y₁ ⟧) : (presheaf_to_yoneda_ob_pstrans_functor Y₁ · # F f) ==> #(y B_is_univalent_2_1 X : psfunctor _ _) f · presheaf_to_yoneda_ob_pstrans_functor Y₂. Proof. use make_nat_trans. - exact (presheaf_to_yoneda_ob_pstrans_nat_trans_data Y₁ Y₂ f). - exact (presheaf_to_yoneda_ob_pstrans_is_nat_trans Y₁ Y₂ f). Defined. Definition presheaf_to_yoneda_ob_pstrans_is_nat_z_iso (Y₁ Y₂ : op1_bicat B) (f : B ⟦ Y₂ , Y₁ ⟧) : is_nat_z_iso (pr1 (presheaf_to_yoneda_ob_pstrans_nat_trans Y₁ Y₂ f)). Proof. intro g ; cbn in g. unfold presheaf_to_yoneda_ob_pstrans_nat_trans. simpl. unfold presheaf_to_yoneda_ob_pstrans_nat_trans_data. pose (is_invertible_2cell_to_is_nat_z_iso (psfunctor_comp F g f)) as i. apply i. exact (psfunctor_comp F g f). Defined. Definition presheaf_to_yoneda_ob_pstrans_data : pstrans_data ((y B_is_univalent_2_1) X) F. Proof. pose x. use make_pstrans_data. - exact presheaf_to_yoneda_ob_pstrans_functor. - intros Y₁ Y₂ f. use make_invertible_2cell. + exact (presheaf_to_yoneda_ob_pstrans_nat_trans Y₁ Y₂ f). + apply is_nat_z_iso_to_is_invertible_2cell. exact (presheaf_to_yoneda_ob_pstrans_is_nat_z_iso Y₁ Y₂ f). Defined. Lemma presheaf_to_yoneda_ob_pstrans_is_pstrans : is_pstrans presheaf_to_yoneda_ob_pstrans_data. Proof. repeat split. - intros Y₁ Y₂ g₁ g₂ α. apply nat_trans_eq. { apply homset_property. } intro h ; cbn in *. unfold presheaf_to_yoneda_ob_pstrans_functor_ob, presheaf_to_yoneda_ob_pstrans_functor_mor, presheaf_to_yoneda_ob_pstrans_nat_trans_data. pose (psfunctor_lwhisker F h α). pose (nat_trans_eq_pointwise p x) as q. exact (!q). - intros Y. apply nat_trans_eq. { apply homset_property. } intro h ; cbn in *. unfold presheaf_to_yoneda_ob_pstrans_functor_ob, presheaf_to_yoneda_ob_pstrans_functor_mor, presheaf_to_yoneda_ob_pstrans_nat_trans_data. refine (!_). etrans. { etrans. { apply maponpaths_2. apply id_left. } etrans. { apply id_left. } exact (nat_trans_eq_pointwise (psfunctor_rinvunitor F h) x). } cbn -[psfunctor_id psfunctor_comp]. apply maponpaths_2. apply id_left. - intros Y₁ Y₂ Y₃ g₁ g₂. apply nat_trans_eq. { apply homset_property. } intro h ; cbn in *. unfold presheaf_to_yoneda_ob_pstrans_functor_ob, presheaf_to_yoneda_ob_pstrans_functor_mor, presheaf_to_yoneda_ob_pstrans_nat_trans_data. refine (!_). etrans. { etrans. { apply maponpaths_2. etrans. { apply id_right. } apply maponpaths_2. etrans. { apply id_right. } apply id_left. } exact (nat_trans_eq_pointwise (psfunctor_rassociator F h g₁ g₂) x). } simpl. etrans. { apply maponpaths_2. apply id_left. } apply idpath. Qed. Definition presheaf_to_yoneda_ob : pstrans (y B_is_univalent_2_1 X) F. Proof. use make_pstrans. - exact presheaf_to_yoneda_ob_pstrans_data. - exact presheaf_to_yoneda_ob_pstrans_is_pstrans. Defined. End PresheafToYonedaOb. Section PresheafToYonedaMor. Variable (a b : (F X : univalent_category)) (f : a --> b). Definition presheaf_to_yoneda_mor_modification_nat_trans_data (Y : op1_bicat B) : nat_trans_data ((presheaf_to_yoneda_ob a) Y : _ ⟶ _) ((presheaf_to_yoneda_ob b) Y : _ ⟶ _) := λ h, #(#F h : _ ⟶ _) f. Lemma presheaf_to_yoneda_mor_modification_is_nat_trans (Y : op1_bicat B) : is_nat_trans _ _ (presheaf_to_yoneda_mor_modification_nat_trans_data Y). Proof. intros h₁ h₂ α ; cbn in *. unfold presheaf_to_yoneda_ob_pstrans_functor_mor, presheaf_to_yoneda_mor_modification_nat_trans_data. pose (pr2 (##F α : _ ⟹ _)) as p. exact (!(p a b f)). Qed. Definition presheaf_to_yoneda_mor_modification_data : modification_data (presheaf_to_yoneda_ob a) (presheaf_to_yoneda_ob b). Proof. intros Y. use make_nat_trans. - exact (presheaf_to_yoneda_mor_modification_nat_trans_data Y). - exact (presheaf_to_yoneda_mor_modification_is_nat_trans Y). Defined. Lemma presheaf_to_yoneda_mor_is_modification : is_modification presheaf_to_yoneda_mor_modification_data. Proof. intros Y₁ Y₂ g. apply nat_trans_eq. { apply homset_property. } intros h ; cbn in *. unfold presheaf_to_yoneda_ob_pstrans_nat_trans_data, presheaf_to_yoneda_mor_modification_nat_trans_data. pose (pr21 (psfunctor_comp F h g)) as p. exact (!(p a b f)). Qed. Definition presheaf_to_yoneda_mor_modification : modification (presheaf_to_yoneda_ob a) (presheaf_to_yoneda_ob b). Proof. use make_modification. - exact presheaf_to_yoneda_mor_modification_data. - exact presheaf_to_yoneda_mor_is_modification. Defined. End PresheafToYonedaMor. Definition presheaf_to_yoneda_data : functor_data (F X : univalent_category) (univ_hom (psfunctor_bicat_is_univalent_2_1 (op1_bicat B) bicat_of_univ_cats univalent_cat_is_univalent_2_1) ((y B_is_univalent_2_1) X) F). Proof. use make_functor_data. - exact presheaf_to_yoneda_ob. - exact presheaf_to_yoneda_mor_modification. Defined. Lemma presheaf_to_yoneda_is_functor : is_functor presheaf_to_yoneda_data. Proof. split. - intros z. apply modification_eq. intros Z. apply nat_trans_eq. { apply homset_property. } intros f. cbn in *. unfold presheaf_to_yoneda_mor_modification_nat_trans_data, presheaf_to_yoneda_ob_pstrans_functor_ob. apply functor_id. - intros z₁ z₂ z₃ f₁ f₂. apply modification_eq. intros Z. apply nat_trans_eq. { apply homset_property. } intros f. cbn in *. unfold presheaf_to_yoneda_mor_modification_nat_trans_data, presheaf_to_yoneda_ob_pstrans_functor_ob. apply functor_comp. Qed. Definition presheaf_to_yoneda : bicat_of_univ_cats ⟦ F X , univ_hom (psfunctor_bicat_is_univalent_2_1 _ _ univalent_cat_is_univalent_2_1) (y B_is_univalent_2_1 X) F ⟧. Proof. use make_functor. - exact presheaf_to_yoneda_data. - exact presheaf_to_yoneda_is_functor. Defined. Definition yoneda_unit_component_mod_component_nat_component (η : pstrans (representable B_is_univalent_2_1 X) F) (Z : op1_bicat B) (f : B ⟦ Z , X ⟧) : pr1 (F Z) ⟦ (η Z : _ ⟶ _) f , (# F f : _ ⟶ _) ((η X : _ ⟶ _) (id₁ X)) ⟧ := #(η Z : _ ⟶ _) (rinvunitor f) · pr1 ((psnaturality_of η f)^-1) (id₁ X). Lemma yoneda_unit_component_mod_component_is_nat_trans (η : pstrans (representable B_is_univalent_2_1 X) F) (Z : op1_bicat B) (f₁ f₂ : B ⟦ Z , X ⟧) (α : f₁ ==> f₂) : # (η Z : _ ⟶ _) α · yoneda_unit_component_mod_component_nat_component η Z f₂ = (yoneda_unit_component_mod_component_nat_component η Z f₁) · (## F α : _ ⟹ _) ((η X : _ ⟶ _) (id₁ X)). Proof. cbn ; unfold yoneda_unit_component_mod_component_nat_component. pose (nat_trans_eq_pointwise (psnaturality_inv_natural η _ _ _ _ α) (id₁ X)). cbn in p. refine (!_). etrans. { refine (!(assoc _ _ _) @ _). apply maponpaths. exact (nat_trans_eq_pointwise (psnaturality_inv_natural η _ _ _ _ α) (id₁ X)). } cbn. refine (assoc _ _ _ @ _ @ !(assoc _ _ _)). apply maponpaths_2. refine (!(functor_comp _ _ _) @ _ @ functor_comp _ _ _). apply maponpaths. refine (!_). refine (rinvunitor_natural _ @ _). apply maponpaths. refine (!_). apply rwhisker_hcomp. Qed. Definition yoneda_unit_component_mod_component_nat (η : pstrans (representable B_is_univalent_2_1 X) F) : modification_data ((functor_identity (hom_data (representable B_is_univalent_2_1 X) F)) η) ((yoneda_to_presheaf ∙ presheaf_to_yoneda) η). Proof. intro Z. use make_nat_trans. - exact (yoneda_unit_component_mod_component_nat_component η Z). - exact (yoneda_unit_component_mod_component_is_nat_trans η Z). Defined. Lemma yoneda_unit_component_is_modification (η : pstrans (representable B_is_univalent_2_1 X) F) : is_modification (yoneda_unit_component_mod_component_nat η). Proof. intros Z₁ Z₂ f. apply nat_trans_eq. { apply homset_property. } intro g ; cbn in g. cbn. unfold yoneda_unit_component_mod_component_nat_component, yoneda_to_presheaf_data_ob, presheaf_to_yoneda_ob_pstrans_nat_trans_data. cbn in f. etrans. { do 2 apply maponpaths. exact (nat_trans_eq_pointwise (pstrans_inv_comp_alt η g f) (id₁ X)). } cbn. rewrite !id_right. rewrite !assoc. apply maponpaths_2. refine (!_). etrans. { apply functor_comp. } apply maponpaths_2. refine (!_). etrans. { apply maponpaths_2. refine (!(assoc _ _ _) @ _). apply maponpaths. etrans. { refine (!_). apply functor_comp. } apply maponpaths. etrans. { apply maponpaths_2. refine (!_). apply rinvunitor_triangle. } cbn. refine (vassocl _ _ _ @ _). etrans. { apply maponpaths. apply lassociator_rassociator. } apply id2_right. } etrans. { apply maponpaths_2. refine (!_). exact (pr21 (psnaturality_of η f) g (g · id₁ X) (rinvunitor g)). } cbn. etrans. { refine (!(assoc _ _ _) @ _). apply maponpaths. exact (nat_trans_eq_pointwise (vcomp_rinv (psnaturality_of η f)) (g · id₁ X)). } apply id_right. Qed. Definition yoneda_unit_component_mod (η : pstrans (representable B_is_univalent_2_1 X) F) : modification (functor_identity (hom_data (representable B_is_univalent_2_1 X) F) η) ((yoneda_to_presheaf ∙ presheaf_to_yoneda) η). Proof. use make_modification. - exact (yoneda_unit_component_mod_component_nat η). - exact (yoneda_unit_component_is_modification η). Defined. Lemma yoneda_unit_is_nat_trans : is_nat_trans (functor_identity (hom_data (representable B_is_univalent_2_1 X) F)) (yoneda_to_presheaf ∙ presheaf_to_yoneda) yoneda_unit_component_mod. Proof. intros η₁ η₂ m. apply modification_eq. intros Z. apply nat_trans_eq. { apply homset_property. } intros g ; cbn in g. cbn. unfold yoneda_unit_component_mod_component_nat_component, yoneda_to_presheaf_data_ob, presheaf_to_yoneda_mor_modification_nat_trans_data, yoneda_to_presheaf_data_mor. refine (!_). etrans. { rewrite <- assoc. apply maponpaths. exact (!(nat_trans_eq_pointwise (mod_inv_naturality_of m X Z g) (id₁ X))). } simpl. rewrite !assoc. apply maponpaths_2. exact (pr2 ((m : modification _ _) Z) _ _ (rinvunitor g)). Qed. Definition yoneda_unit : functor_identity _ ⟹ yoneda_to_presheaf ∙ presheaf_to_yoneda. Proof. use make_nat_trans. - exact yoneda_unit_component_mod. - exact yoneda_unit_is_nat_trans. Defined. Lemma yoneda_unit_is_inverses (g : pstrans (representable B_is_univalent_2_1 X) F) (Z : B) (Y : Z --> X) : is_inverse_in_precat (# (g Z : _ ⟶ _) (rinvunitor Y) · pr1 ((psnaturality_of g Y) ^-1) (id₁ X)) ((pr11 (psnaturality_of g Y)) (id₁ X) · # (g Z : _ ⟶ _) (runitor Y)). Proof. split. - rewrite <- !assoc. etrans. { apply maponpaths. etrans. { rewrite assoc. apply maponpaths_2. exact (nat_trans_eq_pointwise (vcomp_linv (psnaturality_of g Y)) (id₁ X)). } apply id_left. } refine (!(functor_comp _ _ _) @ _ @ functor_id (g Z) _). apply maponpaths. exact (rinvunitor_runitor Y). - rewrite <- !assoc. etrans. { apply maponpaths. etrans. { rewrite assoc. apply maponpaths_2. refine (!(functor_comp (g Z) _ _) @ _ @ functor_id (g Z) _). apply maponpaths. apply runitor_rinvunitor. } apply id_left. } exact (nat_trans_eq_pointwise (vcomp_rinv (psnaturality_of g Y)) (id₁ X)). Qed. Definition yoneda_unit_z_iso (g : pstrans (representable B_is_univalent_2_1 X) F) (Z : B) (Y : Z --> X) : is_z_isomorphism (# (g Z : _ ⟶ _) (rinvunitor Y) · pr1 ((psnaturality_of g Y) ^-1) (id₁ X)). Proof. use tpair. - exact (pr11 (psnaturality_of g Y) (id₁ X) · #(g Z : _ ⟶ _) (runitor Y)). - exact (yoneda_unit_is_inverses g Z Y). Defined. Definition yoneda_counit_component (Z : pr1 (F X)) : pr1 (F X) ⟦ (# F (id₁ X) : _ ⟶ _) Z, Z ⟧ := pr1 ((psfunctor_id F X)^-1) Z. Lemma yoneda_counit_is_natural : is_nat_trans _ (functor_identity _) yoneda_counit_component. Proof. intros Z₁ Z₂ h ; cbn. unfold yoneda_counit_component. pose (pr2 ((psfunctor_id F X)^-1) _ _ h) as p. exact p. Qed. Definition yoneda_counit : presheaf_to_yoneda ∙ yoneda_to_presheaf ⟹ functor_identity _. Proof. use make_nat_trans. - exact yoneda_counit_component. - exact yoneda_counit_is_natural. Defined. Definition bicategorical_yoneda_lemma : left_adjoint_equivalence yoneda_to_presheaf. Proof. apply equiv_to_isadjequiv. use tpair. - use tpair. + exact presheaf_to_yoneda. + split. * exact yoneda_unit. * exact yoneda_counit. - split. + cbn. apply is_nat_z_iso_to_is_invertible_2cell. intro g. apply is_inv2cell_to_is_z_iso. apply make_is_invertible_modification. intro Z. apply is_nat_z_iso_to_is_invertible_2cell. intros Y. exact (yoneda_unit_z_iso g Z Y). + apply is_nat_z_iso_to_is_invertible_2cell. intros Z ; cbn. unfold yoneda_counit_component. exists (pr1 (pr1 (psfunctor_id F X)) Z). split. * abstract (exact (nat_trans_eq_pointwise (vcomp_linv (psfunctor_id F X)) Z)). * abstract (exact (nat_trans_eq_pointwise (vcomp_rinv (psfunctor_id F X)) Z)). Defined. Definition bicategorical_yoneda_lemma_inv : left_adjoint_equivalence presheaf_to_yoneda := inv_adjequiv (_ ,, bicategorical_yoneda_lemma). End YonedaLemma. Section YonedaLocalEquivalence. Context {B : bicat}. Variable (B_is_univalent_2_1 : is_univalent_2_1 B) (X Y : B). Definition yoneda_to_presheaf_representable_component_mod_component_nat (f : X --> Y) (Z : B) (g : Z --> X) : g · f ==> g · f := id₂ (g · f). Lemma yoneda_to_presheaf_representable_component_mod_is_nat_trans (f : X --> Y) (Z : B) : is_nat_trans (representable1 B_is_univalent_2_1 f Z : _ ⟶ _) (presheaf_to_yoneda_ob B_is_univalent_2_1 (representable B_is_univalent_2_1 Y) X f Z : _ ⟶ _) (yoneda_to_presheaf_representable_component_mod_component_nat f Z). Proof. intros h₁ h₂ α. cbn in *. unfold yoneda_to_presheaf_representable_component_mod_component_nat. rewrite id2_left,id2_right. apply idpath. Qed. Definition yoneda_to_presheaf_representable_component_mod_component (f : X --> Y) : modification_data (representable1 B_is_univalent_2_1 f) (presheaf_to_yoneda_ob B_is_univalent_2_1 (representable B_is_univalent_2_1 Y) X f). Proof. intros Z. use make_nat_trans. - exact (yoneda_to_presheaf_representable_component_mod_component_nat f Z). - exact (yoneda_to_presheaf_representable_component_mod_is_nat_trans f Z). Defined. Lemma yoneda_to_presheaf_representable_is_modification (f : X --> Y) : is_modification (yoneda_to_presheaf_representable_component_mod_component f). Proof. intros Z₁ Z₂ h. apply nat_trans_eq. { apply homset_property. } intros g. cbn in *. unfold yoneda_to_presheaf_representable_component_mod_component_nat. rewrite id2_right, lwhisker_id2, id2_left. apply idpath. Qed. Definition yoneda_to_presheaf_representable_component_mod (f : X --> Y) : modification (Fmor (y B_is_univalent_2_1) X Y f) ((presheaf_to_yoneda B_is_univalent_2_1 (representable B_is_univalent_2_1 Y) X : _ ⟶ _) f). Proof. use make_modification. - exact (yoneda_to_presheaf_representable_component_mod_component f). - exact (yoneda_to_presheaf_representable_is_modification f). Defined. Lemma yoneda_to_presheaf_representable_is_natural : is_nat_trans (Fmor_data (y B_is_univalent_2_1) X Y) _ yoneda_to_presheaf_representable_component_mod. Proof. intros g₁ g₂ α. apply modification_eq. intros Z. apply nat_trans_eq. { apply homset_property. } intros h. cbn in *. unfold yoneda_to_presheaf_representable_component_mod_component_nat. rewrite id2_right, id2_left. apply idpath. Qed. Definition yoneda_to_presheaf_representable : (Fmor_univ (y B_is_univalent_2_1) X Y _ _) ⟹ (presheaf_to_yoneda B_is_univalent_2_1 (representable B_is_univalent_2_1 Y) X : _⟶ _). Proof. use make_nat_trans. - exact yoneda_to_presheaf_representable_component_mod. - exact yoneda_to_presheaf_representable_is_natural. Defined. Definition yoneda_to_presheaf_representable_is_iso : @is_invertible_2cell bicat_of_univ_cats _ _ (Fmor_univ (y B_is_univalent_2_1) X Y _ _ : _ ⟶ _) _ (yoneda_to_presheaf_representable). Proof. apply is_nat_z_iso_to_is_invertible_2cell. intro g. apply is_inv2cell_to_is_z_iso. apply make_is_invertible_modification. intro Z. apply is_nat_z_iso_to_is_invertible_2cell. intros h. cbn in *. unfold yoneda_to_presheaf_representable_component_mod_component_nat. apply is_inv2cell_to_is_z_iso. is_iso. Defined. Definition yoneda_mor_is_equivalence : @left_adjoint_equivalence bicat_of_univ_cats _ _ (Fmor_univ (y B_is_univalent_2_1) X Y B_is_univalent_2_1 (psfunctor_bicat_is_univalent_2_1 (op1_bicat B) _ univalent_cat_is_univalent_2_1)). Proof. apply equiv_to_isadjequiv. exact (@left_equivalence_invertible bicat_of_univ_cats _ _ _ (presheaf_to_yoneda B_is_univalent_2_1 (representable B_is_univalent_2_1 Y) X : _⟶ _) (bicategorical_yoneda_lemma_inv B_is_univalent_2_1 _ _) _ yoneda_to_presheaf_representable_is_iso). Defined. End YonedaLocalEquivalence. Definition yoneda_local_equivalence {B : bicat} (B_is_univalent_2_1 : is_univalent_2_1 B) : local_equivalence B_is_univalent_2_1 (psfunctor_bicat_is_univalent_2_1 (op1_bicat B) _ univalent_cat_is_univalent_2_1) (y B_is_univalent_2_1). Proof. intros x y. apply yoneda_mor_is_equivalence. Defined. Definition rezk_completion_2_0 (B : bicat) (HB : is_univalent_2_1 B) : ∑ (GC : bicat) (CB : psfunctor B GC) (HGC : is_univalent_2 GC), weak_equivalence HB (pr2 HGC) CB. Proof. refine (full_image (y HB) ,, _). refine (corestrict_full_image (y HB) ,, _). use tpair. - apply is_univalent_2_full_image. apply psfunctor_bicat_is_univalent_2. exact univalent_cat_is_univalent_2. - exact (corestrict_full_image_weak_equivalence (y HB) HB _ _ (yoneda_local_equivalence HB)). Defined.