Proposition composition_preserves_chosen_terminal_eq {C₁ C₂ C₃ : category} {F : C₁ ⟶ C₂} {G : C₂ ⟶ C₃} {T₁ : Terminal C₁} {T₂ : Terminal C₂} {T₃ : Terminal C₃} (HF : preserves_chosen_terminal_eq F T₁ T₂) (HG : preserves_chosen_terminal_eq G T₂ T₃) : preserves_chosen_terminal_eq (F ∙ G) T₁ T₃. Proof. revert HF. use factor_through_squash. { apply propproperty. } intro p. revert HG. use factor_through_squash. { apply propproperty. } intro q. cbn. apply hinhpr. rewrite p, q. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Adjunctions.Core.