Definition nat_trans_comp {C:precategory_data}{C' : precategory} (F G H: functor_data C C') (a : nat_trans F G) (b : nat_trans G H): nat_trans F H := tpair _ _ (is_nat_trans_comp a b).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence.