Definition one_types_is_univalent_2_1 : is_univalent_2_1 one_types. Proof. intros X Y f g. use isweq_iso. - intros α. apply funextsec. apply α. - intros p. induction p ; cbn. change (homotrefl f) with (toforallpaths _ f f (idpath f)). apply funextsec_toforallpaths. - intros α. cbn. use subtypePath ; cbn. + intro. exact (@isaprop_is_invertible_2cell one_types X Y f g _). + etrans. 2:{ apply toforallpaths_funextsec. } unfold idtoiso_2_1, toforallpaths. cbn. apply funextsec. intro x. induction (funextsec _ f g (pr1 α)). apply idpath. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique.