fact: Variable TA' : NaturalTransformation (S'' o AF') (CF' o S').
imports: Functor.Core NaturalTransformation.Core Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws Functor.Paths Category.Strict HoTT.Tactics PathGroupoids Types.Forall