Definition make_comp_cat_tm {C : comp_cat} {Γ : C} {A : ty Γ} (t : Γ --> Γ & A) (p : t · π A = identity Γ) : comp_cat_tm Γ A := t ,, p. Coercion comp_cat_tm_to_mor {C : comp_cat} {Γ : C} {A : ty Γ} (t : comp_cat_tm Γ A) : Γ --> Γ & A. Proof. exact (pr1 t). 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.