{s d : category F} : s = d <~> (s <~=~> d)%category. Proof. refine (isequiv_sigma_category_isomorphism^-1 oE _ oE (equiv_ap' (issig_pair F)^-1 s d)). refine (_ oE (equiv_path_sigma _ _ _)^-1). simpl. simple refine (equiv_functor_sigma' _ _). { exists (@idtoiso C _ _). exact _. } { exact category_isotoid_helper. } Defined.
Require Import Category.Core Functor.Core. Require Import Category.Univalent. Require Import Category.Morphisms. Require Import SetCategory.Core. Require Import Grothendieck.ToSet.Core Grothendieck.ToSet.Morphisms. Require Import HoTT.Basics.Equivalences HoTT.Basics.Trunc. Require Import HoTT.Types.Universe HoTT.Types.Sigma.