Definition op1_bicat_is_univalent_2_0 {C : bicat} (C_is_univalent_2_1 : is_univalent_2_1 C) (C_is_univalent_2_0 : is_univalent_2_0 C) : is_univalent_2_0 (op1_bicat C). Proof. intros X Y. use weqhomot. - exact (op1_bicat_idtoiso_2_0_alt C_is_univalent_2_0 X Y). - intros p. induction p. use subtypePath. { intro ; apply isaprop_left_adjoint_equivalence. apply op1_bicat_is_univalent_2_1. exact C_is_univalent_2_1. } 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.opp_precat. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInOp1Bicat. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat.