Definition ptd_comp {F F' F'' : ptd_obj} (α : ptd_mor F F') (α' : ptd_mor F' F'') : ptd_mor F F''. Proof. exists (nat_trans_comp _ _ _ α α'). abstract ( intro c; simpl; rewrite assoc ; set (H:=ptd_mor_commutes α c); simpl in H; rewrite H; clear H ; set (H:=ptd_mor_commutes α' c); simpl in H; rewrite H; clear H ; apply idpath ). Defined.
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.FunctorCategory.