{A B} {F G H : A -> B} `{IsGraph A} `{HasEquivs B} `{!Is0Functor F, !Is0Functor G, !Is0Functor H} (alpha : NatEquiv G H) (beta : NatEquiv F G) : NatEquiv F H := Build_NatEquiv' (nattrans_comp alpha beta).
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Square. Require Import WildCat.Opposite.