{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. Proof. apply equiv_path. apply ap10, ap. destruct a; simpl. exact (ap10 (identity_of F _)^ _). 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.