proposition: Lemma isaprop_is_invertible_2cell {C : bicat} {a b : C} {f g : C ⟦a, b⟧} (x : f ==> g) : isaprop (is_invertible_2cell x).
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct