Definition lan_precomposition_counit_point (F : C₂ ⟶ D) (x : C₂) : lan_point ColimsD P (P ∙ F) x --> F x. Proof. use colim_mor. - exact (λ v, #F (pr2 v)). - abstract (intros v₁ v₂ e ; refine (!(functor_comp F _ _) @ maponpaths (λ z, #F z) _) ; exact (!(pr2 e) @ id_right _)). 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.