Proposition eq_sub_to_extension {C : comp_cat} {Γ Δ : C} {A : ty Γ} {s₁ s₂ : Δ --> Γ & A} (p : s₁ · π _ = s₂ · π _) (q : transport_term_sub_eq p (sub_to_extension_tm s₁) = sub_to_extension_tm s₂) : s₁ = s₂. Proof. pose (maponpaths (λ z, pr1 z · PullbackPr1 (comp_cat_pullback _ _)) q) as q'. simpl in q'. rewrite !PullbackArrow_PullbackPr1 in q'. refine (_ @ q'). enough (s₁ = sub_to_extension_tm s₁ · comp_cat_extend_over A (s₁ · π A)) as H. { exact H. } clear p q q' s₂. refine (!_). apply (PullbackArrow_PullbackPr1 (comp_cat_pullback A (s₁ · π A))). Qed.
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.