Definition three_isColimCocone : isColimCocone d three_colimit three_cocone. Proof. intros c cc. transparent assert (ccbase : (cocone dbase (three_mor02 c))). { exists (λ v, pr1 (coconeIn cc v)). abstract ( intros u v e; exact (base_paths _ _ (coconeInCommutes cc _ _ e)) ). } transparent assert (cc11 : (cocone d11 (three_ob1 c))). { exists (λ v, three_mor11 (coconeIn cc v)). intros u v e. set (ob1_path := base_paths _ _ (fiber_paths (coconeInCommutes cc _ _ e))). abstract ( apply pathsinv0; etrans; [exact (pathsinv0 ob1_path)|]; cbn; rewrite pr1_transportf; rewrite transportf_const; reflexivity ). } use unique_exists. - exists (colimArrow clbase _ ccbase). exists (colimArrow cl11 _ cc11). split. * abstract ( etrans; [use precompWithColimOfArrows|]; apply pathsinv0; etrans; [use postcompWithColimArrow|]; apply maponpaths; (apply subtypePath; [intro; do 3 (apply impred; intro); apply homset_property|]); apply funextsec; intro v; exact (pathsinv0 (pr1 (three_mor_comm (coconeIn cc v)))) ). * abstract ( etrans; [use precompWithColimOfArrows|]; apply pathsinv0; etrans; [use postcompWithColimArrow|]; apply maponpaths; (apply subtypePath; [intro; do 3 (apply impred; intro); apply homset_property|]); apply funextsec; intro v; exact (pathsinv0 (pr2 (three_mor_comm (coconeIn cc v)))) ). - abstract ( intro; use three_mor_eq''; [ exact (colimArrowCommutes clbase _ ccbase v)| exact (colimArrowCommutes cl11 _ cc11 v) ] ). - abstract ( intro; apply impred; intro; apply homset_property ). - abstract ( intros y H; use three_mor_eq''; apply colimArrowUnique; intro v; [ exact (base_paths _ _ (H v))| ]; apply pathsinv0; etrans; [exact (pathsinv0 (base_paths _ _ (fiber_paths (H v))))|]; etrans; [ cbn; rewrite pr1_transportf; rewrite transportf_const; reflexivity| ]; reflexivity ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Arrow.