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