Definition lan_mor : D ⟦ lan_point x , lan_point y ⟧. Proof. refine (colim_mor (lan_colim x) (lan_point y) (λ v, lan_mor_cocone_ob (pr11 v) (pr2 v)) (λ v₁ v₂ e, lan_mor_forms_cocone (pr2 v₁) (pr2 v₂) (pr11 e) _)). abstract (exact(!(id_right _) @ pr2 e)). 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.