(x : Functor C'' D) : G' o G o x o (F' o F) = G' o (G o x o F') o F. Proof. path_functor. Defined.
Require Import Category.Core Functor.Core Functor.Pointwise.Core NaturalTransformation.Core NaturalTransformation.Paths Functor.Composition.Core Functor.Identity Functor.Paths. Require Import PathGroupoids Types.Forall HoTT.Tactics. Require Import Basics.Tactics.