(x y : C) (H : x = y) : Isomorphic x y := match H in (_ = y0) return (x <~=~> y0) with | 1%path => reflexivity x end.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.