fact: 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).
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets