Solution to exercise 1.1

This is a literate Rzk file:

#lang rzk-1

Problem statement

Exercise 1.1

Given functions \(f : A \to B\) and \(g : B \to C\), define their composite \(g \circ f : A \to C\). Show that we have \(h \circ (g \circ f) \equiv (h \circ g) \circ f\).

Solution

First, the definition of the composition operation is provided as:

\[ g \circ f :\equiv \lambda (x: A) . g(f(x)) \]

Then, associativity can be demonstrated by evaluating both sides of the equality and reaching the same result:

\[ \begin{align*} h \circ (g \circ f) & \equiv \lambda x. h((g\circ f)(x)) \\ & \equiv \lambda x. h((\lambda x' . g(f(x'))) (x)) \\ & \equiv \lambda x. h(g(f(x))) \end{align*} \]

\[ \begin{align*} (h \circ g) \circ f & \equiv \lambda x. (h\circ g)(f(x)) \\ & \equiv \lambda x. (\lambda y . h(g(y)))(f(x)) \\ & \equiv \lambda x. h(g(f(x))) \end{align*} \]

This can be represented in rzk like so:

#define compose
  ( A B C : U)
  ( g : B → C)
  ( f : A → B)
  : A → C
  := \ x → g (f x)

Associativity is automatic (by refl):

#define composition-associativity
  ( A B C D : U)
  ( f : A → B)
  ( g : B → C)
  ( h : C → D)
  : compose A C D h (compose A B C g f) = compose A B D (compose B C D h g) f
  := refl

An explicit proof (not checked by rzk):

compose A C D h (compose A B C g f)
= \ x → h ((compose A B C g f) x)       (unfolding compose)
= \ x → h ((\ x2 → g (f x2)) x)         (unfolding compose)
= \ x → h (g (f x))                     (beta reduction)
= \ x → (\ x2 → h (g x2)) (f x)         (beta reduction)
= \ x → (compose B C D h g) (f x)       (fold compose)
= compose A B D (compose B C D h g) f   (fold compose)