Definition sub_to_extension_tm {C : comp_cat} {Γ Δ : C} {A : ty Γ} (s : Δ --> Γ & A) : comp_cat_tm Δ (A [[ s · π _ ]]). Proof. use make_comp_cat_tm. - use (PullbackArrow (comp_cat_pullback _ _)). + exact s. + apply identity. + abstract (rewrite id_left ; apply idpath). - 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.