Definition lan_mor_forms_cocone {z₁ z₂ : C₁} (h₁ : P z₁ --> x) (h₂ : P z₂ --> x) (e : z₁ --> z₂) (p : h₁ = # P e · h₂) : # F e · lan_mor_cocone_ob z₂ h₂ = lan_mor_cocone_ob z₁ h₁. Proof. refine (colimInCommutes (lan_colim y) ((z₁ ,, tt) ,, h₁ · f) ((z₂ ,, tt) ,, h₂ · f) ((e ,, idpath _) ,, _)). abstract (cbn ; rewrite id_right ; rewrite !assoc ; apply maponpaths_2 ; exact p). Defined.
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.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.CommaCategories. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.