Definition is_univalent_sigma_of_twosided_disp_cat_help (HD₂ : is_univalent_disp D₂) {x₁ : C₁} {y₁ : C₂} (xy₁ xy₂ : sigma_twosided_disp_cat x₁ y₁) (p : pr1 xy₁ = pr1 xy₂) : (transportf (λ z, D₂ (x₁ ,, y₁ ,, z)) p (pr2 xy₁) = pr2 xy₂) ≃ z_iso_disp (@make_z_iso_total_twosided_disp_cat _ _ D₁ _ _ _ _ _ _ _ _ (idtoiso_twosided_disp (idpath _) (idpath _) p)) (pr2 xy₁) (pr2 xy₂). Proof. induction xy₁ as [ z₁ z₂ ]. induction xy₂ as [ z₃ z₄ ]. cbn in *. induction p ; cbn. refine (_ ∘ (_ ,, HD₂ _ _ (idpath _) z₂ z₄))%weq. use weq_iso. - intro f. simple refine (pr1 f ,, pr12 f ,, _ ,, _). + abstract (refine (pr122 f @ _) ; apply transportf_hset_eq ; apply homset_property). + abstract (refine (pr222 f @ _) ; apply transportf_hset_eq ; apply homset_property). - intro f. simple refine (pr1 f ,, pr12 f ,, _ ,, _). + abstract (refine (pr122 f @ _) ; apply transportf_hset_eq ; apply (total_twosided_disp_category D₁)). + abstract (refine (pr222 f @ _) ; apply transportf_hset_eq ; apply (total_twosided_disp_category D₁)). - abstract (intro f ; use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ; apply idpath). - abstract (intro f ; use subtypePath ; [ intro ; apply (@isaprop_is_z_iso_disp _ D₂) | ] ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Section FromSigmaIso. End FromSigmaIso.