Definition transportf_dirprod_fam {X : UU} {Y₁ Y₂ : X → UU} {x₁ x₂ : X} (p : x₁ = x₂) (y : Y₁ x₁ × Y₂ x₁) : transportf (λ x, Y₁ x × Y₂ x) p y = transportf Y₁ p (pr1 y) ,, transportf Y₂ p (pr2 y). Proof. induction p. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.