{s d} : @Isomorphic A' s d -> @Isomorphic A s d. Proof. refine ((issig_full_isomorphic A _ _) o _ o (issig_full_isomorphic A' _ _)^-1). exact (functor_sigma pr1_type (fun _ => functor_sigma pr1_type (fun _ => functor_sigma pr1_path (fun _ => pr1_path)))). Defined.
Require Import Category.Core Category.Morphisms. Require Import Category.Univalent. Require Import Category.Sigma.Core Category.Sigma.OnObjects Category.Sigma.OnMorphisms. Require Import HoTT.Types HoTT.Basics.