Definition transport_term_sub_eq {C : comp_cat} {Γ Δ : C} {s₁ s₂ : Δ --> Γ} (p : s₁ = s₂) {A : ty Γ} (t : comp_cat_tm Δ (A [[ s₁ ]])) : comp_cat_tm Δ (A [[ s₂ ]]). Proof. use make_comp_cat_tm. - use (PullbackArrow (comp_cat_pullback _ _)). + exact (t · comp_cat_extend_over _ _). + apply identity. + abstract (induction p ; rewrite id_left ; rewrite !assoc' ; unfold comp_cat_extend_over ; refine (maponpaths (λ z, _ · z) (comprehension_functor_mor_comm _ _) @ _) ; rewrite !assoc ; refine (maponpaths (λ z, z · _) (comp_cat_tm_eq t) @ _) ; apply id_left). - abstract (apply (PullbackArrow_PullbackPr2 (comp_cat_pullback _ _))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.