Can we somehow get functoriality from purely type-theoretic reasoning?
There are two senses in which type formation operations are 'functorial,' but neither matches functoriality on the category of types.
First, you can interpret the collection of types as a groupoid, and consider isomorphisms between types to be 'arrows.' These compose, but also always have inverses, so are in some sense undirected. However, this is also why all constructions are able to be functorial, because type formation operations have both covariant and contravariant positions, and thus may not preserve the direction of arrows.
Anyhow, functoriality here says that if you have $P : A \cong B$ then there is always $F P : F A \cong F B$, and: $$F\ \mathsf{Refl}_A = \mathsf{Refl}_{F A} \\ F (P \cdot Q) = F P \cdot F Q$$ This is essentially the direction of homotopy type theory, where these properties are internalized (and the 'dimension' is not limited to just groupoids).
The second functoriality property is already in the other answer. The &quot;identity extension lemma&quot; is a functoriality property where categories are relaxed to reflextive graphs (rather than tightened to groupoids). Again, type formation operations are able to be functorial because reflexive graphs do not have operations where 'direction' matters. However, this time it is because edges are not assumed to be composible.
So, the identity extension lemma says that every relation $R : A \Leftrightarrow B$ induces a relation $FR : FA \Leftrightarrow FB$ where:
$$F\ \mathsf{Refl}_A = \mathsf{Refl}_{F A}$$
And that's all there is to being a &quot;relator&quot; of reflexive graphs. There are also type systems that can talk about this sort of thing internally, possibly even with homotopy type theory features, like here.
Now, The first approach doesn't give you 'normal' functoriality for all type formations because not every map $f : A → B$ is an isomorphism. And of course, if we do $F A = A → A$, that's not going to extend to $(A → A) → (B → B)$ nor the other direction, without also having some map in the other direction. However, given an isomorphism, it induces $(A → A) \cong (B → B)$
In the second approach, a map $f : A → B$ induces a relation $\mathsf{gr} f : A \Leftrightarrow B$ given by $(x, f\ x)$. However, although we could compose the maps, there is no notion of composition of relations to talk about, and relate back to the composed functions. Considering the same type construction:
$$FR(m,n)\quad \Longleftrightarrow \quad R(x,y) ⇒ R(m\ x, n\ y)$$
So:
$$F(\mathsf{gr}\ f)(m,n)\quad \Longleftrightarrow\quad f \circ m = n \circ f$$
If you try to apply this to composed maps, then you know:
$$f \circ m = n \circ f \\ g \circ m = n \circ g$$
so $$f \circ g \circ m = f \circ n \circ g$$
but then there's nothing to do further.
You can read more about this angle in this paper, which tries to apply parametricity to a wider mathematical scope. A counter-question that the paper kind of motivates is: why do you care specifically about category functoriality? The original intuitive specification of &quot;naturality&quot; sounds very much like the intuitive specification of &quot;parametricity,&quot; but the former was eventually formalized in terms of directed maps, rather than undirected relations. However, there is nothing inherently more legitimate about directed maps vs. relations or isomorphisms, and some things work out more appropriately for the latter than the former. Sometimes even in category theory it it necessary to shift into the 'undirected' perspective to make easier sense of something. See for instance here.
On a final note, you can have a type theory that keeps track of category theoretic functoriality of things. Here is early work, and here is something closer to homotopy type theory. The former tracks functoriality of everything explicitly, and is of course significantly more complicated for it. The latter allows functoriality to be an internally definable property, similar to the 'dimension' in homotopy type theory. But in neither would every type expression be necessarily functorial with respect to directed maps, because that would require limiting what one is able to write.