proposition: Lemma path_idtoequiv_idtoiso (s d : set_cat) (p : s = d) : iso_equiv s d (equiv_path _ _ (ap trunctype_type p)) = idtoiso set_cat p.
proof: Proof. apply path_isomorphic. case p. reflexivity. Defined.
imports: Category.Core NaturalTransformation.Core Category.Morphisms NaturalTransformation.Paths Category.Univalent SetCategory.Core HoTT.Basics HoTT.Types TruncType