proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.Limits.Pullbacks UniMath.Bicategories.ComprehensionCat.BicatOfCompCat