Lemma nat_trans_comp_pointwise (C : precategory_data)(C' : precategory) (hs: has_homsets C') (F G H : ob [C, C', hs]) (A : F --> G) (A' : G --> H) (B : F --> H) : A · A' = B -> ∏ a, pr1 A a · pr1 A' a = pr1 B a. Proof. intros H' a. intermediate_path (pr1 (A · A') a). apply idpath. destruct H'. apply idpath. Qed.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence.