Library UniMath.CategoryTheory.PointedFunctorsComposition


**********************************************************
Benedikt Ahrens, Ralph Matthes
SubstitutionSystems
2015
**********************************************************
Contents :
  • Definition of composition of pointed functors

Require Import UniMath.Foundations.PartD.

Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.PointedFunctors.
Require Import UniMath.CategoryTheory.HorizontalComposition.

Section def_ptd.

Variable C : precategory.
Variable hs : has_homsets C.

Definition ptd_composite (Z Z' : ptd_obj C) : precategory_Ptd C hs.
Proof.
   (functor_composite Z Z').
  apply (horcomp (ptd_pt _ Z) (ptd_pt _ Z')).
Defined.

End def_ptd.