Proposition weighted_hom_co_is_functor (w : C) : is_functor (weighted_hom_co_data w). Proof. split. - intro i ; cbn. rewrite !functor_id. rewrite precomp_arr_id. rewrite (functor_id W). rewrite internal_pre_post_comp_id. apply idpath. - intros i j k f g ; cbn. refine (_ @ internal_pre_post_comp_comp _ _ _ _). rewrite !functor_comp. rewrite !precomp_arr_comp. pose (functor_comp W (pr2 g) (pr2 f)) as p. cbn in p. rewrite p. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Ends. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedConicalColimits. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers. Import MonoidalNotations.