Library UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors

********************************************************** Benedikt Ahrens, Ralph Matthes 2015 Modified by: Anders Mörtberg, 2016 Ralph Matthes, 2017 ********************************************************** Contents :

• Definition of the (weak) monoidal structure on endofunctors (however, the definitions are not confined to endofunctors)
  Here, we only give the unitors and associators and do not build a monoidal category (anyway, this is not possible since we are not considering only endofunctors).

There is a monoidal structure on endofunctors, given by composition. While this is considered to be strict in set-theoretic category theory, it ain't strict in type theory with respect to convertibility. So we consider it to be a weak monoidal structure instead. However, pointwise, it suffices to take the identity for all those natural transformations (the identity is also behind the definition of nat_trans_functor_assoc). To understand the need for this structure even better, notice that the proofs of functor axioms for one composition in the unitality and associativity properties are slightly different from the proofs for the other and because of it the composition of functors is not strictly unital or associative. However, these proofs are not used in the definition of natural transformations, to be precise only functor_data is used, and the composition of functor_data is strictly unital and associative.

while this is normally used for endofunctors, it can be done more generally, but already for endofunctors, this is crucial for the development of substitution systems

this also holds in the target but is not needed here

trivially, this observed convertibility implies the following three convertibilities

again, this also holds in the target but is not needed here

end of implied convertibilities the last convertibility fails for the composition with the identity as second argument

in particular, there is no convertibility between the arguments to H

as a motivation, we show here that, propositionally, the functors in source and target of these are equal, for each of the three pairs of functors; the extra assumption on having homsets is only used in order to have simple proofs, it is not necessary, as shown below

these laws do not help in type-checking definitions which is why the transformations further above are needed now we get rid of the homset assumptions by using results of Section "functor_equalities" in UniMath.CategoryTheory.Core.Functors.v