Lemma isaprop_is_invertible_2cell {C : bicat} {a b : C} {f g : C ⟦a, b⟧} (x : f ==> g) : isaprop (is_invertible_2cell x). Proof. apply invproofirrelevance. intros p q. apply subtypePath. { intro. apply isapropdirprod; apply cellset_property. } set (Hz1 := pr12 q). set (Hy2 := pr22 p). set (y := pr1 p). set (z := pr1 q). cbn in *. intermediate_path (y • (x • z)). - apply pathsinv0. etrans. { apply maponpaths. apply Hz1. } apply id2_right. - etrans. { apply vassocr. } etrans. { apply maponpaths_2. apply Hy2. } apply id2_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.