Definition ps_base_is_univalent_2_1 (HD_2_1 : is_univalent_2_1 D) : is_univalent_2_1 ps_base. Proof. intros F G η ε. use weqhomot. - simple refine (invertible_2cell_ps_base_weq η ε ∘ _)%weq. simple refine (_ ∘ make_weq _ (isweqtoforallpaths _ _ _))%weq. simple refine (weqonsecfibers _ _ _). intro X ; cbn. exact (make_weq (idtoiso_2_1 (η X) (ε X)) (HD_2_1 _ _ _ _)). - intros p. induction p. use subtypePath. { intro ; apply isaprop_is_invertible_2cell. } reflexivity. 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.PrecategoryBinProduct. 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.Core.AdjointUnique.