Definition double_transport_disp {C C':category} {D':disp_cat C'} {a b a' b':C} (F:functor C C') (f:a-->b) (x:D' (F a)) (y:D' (F b)) (p:a=a') (q:b=b') : x-->[#F f]y -> transportf (λ z, D' (F z)) p x -->[# F (double_transport p q f)] transportf (λ z, D' (F z)) q y. Proof. intro Df. destruct p, q. exact Df. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering.