proposition: Lemma idtoiso_inv (C : PreCategory) (s d : C) (p : s = d) : (idtoiso _ p)^-1 = idtoiso _ (p^)%path.
proof: Proof. path_induction; reflexivity. Defined.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences