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.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.PointedFunctors.
Require Import UniMath.CategoryTheory.HorizontalComposition.
Section def_ptd.
Variable C : category.
Definition ptd_composite (Z Z' : ptd_obj C) : category_Ptd C.
Show proof.
Definition ptd_compose (Z Z' : ptd_obj C) : category_Ptd C.
Show proof.
exists (functor_compose (pr1 Z:[C, C]) (pr1 Z':[C, C])).
apply (# (functorial_composition _ _ _) (((ptd_pt _ Z: [C, C]⟦functor_identity C,pr1 Z⟧) ,,
(ptd_pt _ Z': [C, C]⟦functor_identity C,pr1 Z'⟧))
: category_binproduct [C, C] [C, C] ⟦(functor_identity C,,functor_identity C),(pr1 Z,,pr1 Z')⟧)).
apply (# (functorial_composition _ _ _) (((ptd_pt _ Z: [C, C]⟦functor_identity C,pr1 Z⟧) ,,
(ptd_pt _ Z': [C, C]⟦functor_identity C,pr1 Z'⟧))
: category_binproduct [C, C] [C, C] ⟦(functor_identity C,,functor_identity C),(pr1 Z,,pr1 Z')⟧)).
Lemma ptd_composite_compose (Z Z' : ptd_obj C): ptd_composite Z Z' = ptd_compose Z Z'.
Show proof.
use total2_paths_f.
- apply idpath.
- cbn.
rewrite (@horcomp_post_pre _ _ C).
apply (nat_trans_eq (homset_property C)).
intro c. apply idpath.
- apply idpath.
- cbn.
rewrite (@horcomp_post_pre _ _ C).
apply (nat_trans_eq (homset_property C)).
intro c. apply idpath.
End def_ptd.