Definition sub_comp_cat_tm {C : comp_cat} {Γ Δ : C} {A : ty Γ} (t : comp_cat_tm Γ A) (s : Δ --> Γ) : comp_cat_tm Δ (A [[ s ]]). Proof. use make_comp_cat_tm. - use (PullbackArrow (comp_cat_pullback A s)). + exact (s · t). + apply identity. + abstract (rewrite id_left ; rewrite !assoc' ; rewrite comp_cat_tm_eq ; apply id_right). - abstract (apply (PullbackArrow_PullbackPr2 (comp_cat_pullback A s))). 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.