Definition hProp_weq (X Y : hProp) : (X ≃ Y) ≃ ((X → Y) × (Y → X)). Proof. use weq_iso. - exact (λ w, pr1 w ,, invmap w). - exact (λ f, weqimplimpl (pr1 f) (pr2 f) (pr2 X) (pr2 Y)). - abstract (intro w ; cbn ; use subtypePath ; [ intro ; apply isapropisweq | ] ; cbn ; apply idpath). - abstract (intro w ; 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.Categories.HSET.Core. 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.TwoSidedFibration.