Definition folds_double_transport {C : folds_3_ob_mor} {a a' b b' : ob C} (p : a = a') (q : b = b') (f : a ⇒ b) : a' ⇒ b' := transportf (λ c, a' ⇒ c) q (transportf (λ c, c ⇒ b) p f).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.