proposition: Lemma isaprop_sigma_z_iso (A B : category) (HA : is_univalent A) (F : functor A B) (HF : fully_faithful F) : ∏ b : ob B, isaprop (∑ a : ob A, z_iso (F a) b).
proof: Proof. intro b. apply invproofirrelevance. intros x x'; destruct x as [a f]; destruct x' as [a' f']. set (fminusf := z_iso_comp f (z_iso_inv_from_z_iso f')). set (g := iso_from_fully_faithful_reflection HF fminusf). apply (two_arg_paths_f (B:=λ a', z_iso (F a') b) (isotoid _ HA g)). intermediate_path (z_iso_comp (z_iso_inv_from_z_iso (functor_on_z_iso F (idtoiso (isotoid _ HA g)))) f). - generalize (isotoid _ HA g). intro p0; destruct p0. rewrite <- functor_on_z_iso_inv. simpl. rewrite z_iso_inv_of_z_iso_id. apply z_iso_eq. simpl; rewrite functor_id. rewrite id_left. apply idpath. - rewrite idtoiso_isotoid. unfold g; clear g. unfold fminusf; clear fminusf. assert (HFg : functor_on_z_iso F (iso_from_fully_faithful_reflection HF (z_iso_comp f (z_iso_inv_from_z_iso f'))) = z_iso_comp f (z_iso_inv_from_z_iso f')). + generalize (z_iso_comp f (z_iso_inv_from_z_iso f')). intro h. apply z_iso_eq; simpl. set (H3:= homotweqinvweq (weq_from_fully_faithful HF a a')). simpl in H3. unfold fully_faithful_inv_hom. unfold invweq; simpl. rewrite H3; apply idpath. + rewrite HFg. rewrite z_iso_inv_of_z_iso_comp. apply z_iso_eq; simpl. repeat rewrite <- assoc. rewrite z_iso_after_z_iso_inv. rewrite id_right. set (H := z_iso_inv_z_iso_inv _ _ f'). now apply (base_paths _ _ H). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core