Is this a valid proof that function composition is associative in type theory? On page 56 of "Homotopy Type Theory" they give the first exercise of defining function composition and proving that it is a associative. So here goes:
$$\circ :\Pi_{g:A\rightarrow B}\Pi_{f:B\rightarrow C}(A\rightarrow C)$$
$\circ$ is a function that takes in two functions and returns another, we will naturally use it as infix and define
$$(f\circ g) (a):=f(g(a))$$
where $a:A$. Now let $h:Z\rightarrow A$, and let $z:Z$ and $a:=h(z)$ then 
$$(f\circ g) (a) := (f\circ g)h(z):=f(g(h(z)))$$
$(f\circ (g\circ h))(z)$ is the application of $f$ to $(g\circ h)(z)$, since $g\circ h$ is $\lambda z.g(h(z))$ we should just be able to apply f then just apply the entire thing to $z$. But this doesn't seem right in the framework of propositions as types. I feel like I'm meant to prove that you can construct an element of the type $(f\circ g)\circ h = f \circ (g\circ h)$. Despite having read the first chapter, I'm not quite sure about how to go about this, hints would be appreciated and please let me know at the top of your post if you intend on giving the full solution.
 A: This is a bit of a mash. So first, given a $z$, $((f \circ g) \circ h)(z)$ and $(f \circ (g \circ h))(z)$ are simply equal.  We say that they are judgementally or definitionally equal. (Usually this can be checked by computing to normal form and verifying that you get the same normal form which is effectively what you did. This is generally a highly mechanical process.) In a proof assistant like Coq or Agda, there is no work to do(; it automatically does the computation).   The proof term for the corresponding identity type is $\mathtt{refl}$.  So, to this extent, you're not missing anything. 
Correction: As Mike Shulman points out, when the pointwise equality is judgemental, function extensionality isn't necessary. So there really is nothing to do but the mechanical exercise of checking whether the two terms have the same normal form. If you want to completely "show your work", you can list out the reductions. I'll leave the following paragraph which is incorrect in stating that function extensionality is necessary, but highlights function extensionality which is a thing you need to be a bit more mindful of in intensional type theories in general and even in HoTT which has it propositionally.

But, this is not the same as saying $(f \circ g) \circ h = f \circ (g
 \circ h)$ as this requires function extensionality given the above
  fact.  Function extensionality typically doesn't hold in intensional
  type theories, and it certainly doesn't hold definitionally, but it
  does hold propositionally in HoTT.  Basically, your proof is a proof
  of $$\prod_{z:Z}((f \circ g) \circ h)(z) =_Z (f \circ (g \circ
 h))(z)$$ via $\lambda z:Z.\mathtt{refl}(z)$ and by applying function
  extensionality you can produce a term of type $(f \circ g) \circ h
 =_{Z\to C} f \circ (g \circ h)$. The proof term would then be something like $\mathtt{funext}(\lambda z:Z.\mathtt{refl}(z))$ though
  you definitely need to provide some additional arguments to
  $\mathtt{funext}$ to actually make this a statement about
  associativity of composition.

