fact: Definition category_isotoid_helper {s d} (a : c s = c d) : (transport (fun c : C => F c) a (x s) = x d) <~> (F _1 (idtoiso C a)) (x s) = x d.
imports: Category.Core Functor.Core Category.Univalent Category.Morphisms SetCategory.Core Grothendieck.ToSet.Core Grothendieck.ToSet.Morphisms HoTT.Basics.Equivalences HoTT.Basics.Trunc HoTT.Types.Universe HoTT.Types.Sigma