Lemma isaprop_cwf_fiber_representation {Γ:C} (A : Ty Γ : hSet) : is_univalent C -> isaprop (cwf_fiber_representation A). Proof. intro isC. apply invproofirrelevance. intros x x'. apply subtypePath. { intro. apply isofhleveltotal2. - apply setproperty. - intro. apply isaprop_isPullback. } destruct x as [x H]. destruct x' as [x' H']. cbn. destruct x as [ΓA m]. destruct x' as [ΓA' m']. cbn in *. destruct H as [H isP]. destruct H' as [H' isP']. use (total2_paths_f). - set (T1 := make_Pullback _ isP). set (T2 := make_Pullback _ isP'). set (i := z_iso_from_Pullback_to_Pullback T1 T2). cbn in i. set (i' := invmap (weq_ff_functor_on_z_iso (yoneda_fully_faithful _) _ _ ) i ). set (TT := isotoid _ isC i'). apply TT. - cbn. set (XT := transportf_dirprod _ (fun a' => C⟦a', Γ⟧) (fun a' => Tm a' : hSet)). cbn in XT. set (XT' := XT (tpair _ ΓA m : ∑ R : C, C ⟦ R, Γ ⟧ × (Tm R : hSet) ) (tpair _ ΓA' m' : ∑ R : C, C ⟦ R, Γ ⟧ × (Tm R : hSet) )). cbn in *. match goal with | [ |- transportf _ ?e _ = _ ] => set (TT := e) end. rewrite XT'. clear XT' XT. destruct m as [π te]. destruct m' as [π' te']. cbn. apply pathsdirprod. + unfold TT; clear TT. rewrite transportf_isotoid. cbn. unfold from_Pullback_to_Pullback. cbn in *. pose (XR' := nat_trans_eq_pointwise (PullbackArrow_PullbackPr1 (make_Pullback _ isP) (yoneda_objects C ΓA') (yoneda_morphisms C ΓA' Γ π') (yoneda_map_2 C ΓA' Tm te') (PullbackSqrCommutes (make_Pullback _ isP'))) ΓA'). cbn in XR'. assert (XR'':= toforallpaths _ _ _ XR'). cbn in XR''. etrans. { apply XR''. } apply id_left. + unfold TT; clear TT. match goal with |[|- transportf ?r _ _ = _ ] => set (P:=r) end. match goal with |[|- transportf _ (_ _ _ (_ _ ?ii)) _ = _ ] => set (i:=ii) end. simpl in i. apply (invmaponpathsweq (@yy _ Tm ΓA')). etrans. { apply transportf_yy. } etrans. { apply (@transportf_functor_isotoid C (functor_category _ SET)). } rewrite inv_from_z_iso_iso_from_fully_faithful_reflection. assert (XX:=homotweqinvweq (weq_from_fully_faithful (yoneda_fully_faithful _) ΓA' ΓA )). etrans. { apply maponpaths_2. apply XX. } clear XX. etrans. { apply maponpaths_2. unfold from_Pullback_to_Pullback. apply idpath. } pose (XR' := PullbackArrow_PullbackPr2 (make_Pullback _ isP) (yoneda_objects C ΓA') (yoneda_morphisms C ΓA' Γ π') (yoneda_map_2 C ΓA' Tm te') (PullbackSqrCommutes (make_Pullback _ isP'))). apply XR'. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.ContravariantFunctor. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Cofunctormap. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat.