#import "@preview/prooftrees:0.1.0": *
#show math.eq: math.scripts
#let prooftree(..args) = tree(
  tree_config: tree_config(
    vertical_spacing: 6pt,
  ),
  ..args
)

= Problem 3

Assume that you have Id but not Eq at your disposal, and you can only use rules. Write down an abstraction unitl ("unitl" for "unit left") such that:

#prooftree(
  axi[$ d ∈ [a =_A b] $],
  uni[$ "unitl"(a, d) ∈ ["trans"(id(a), d) =_[a =_A b] d] $],
)

There's a trick here that you may notice if you remember the definition of "trans" and the computation rule for "idpeel":

$
  "trans"(d,e) ≡ "apply"("idpeel"(d,(x)lambda y.y),e)
$

// #tree(
//   axi[$a in A$],
//   axi[$b in A$],
//   axi[$c in "Id"(A, a, b)$],
//   axi[$C(x, y, z) "set" [x in A, y in A, z in "Id"(A, x, y)]$],
//   axi[$d(x) in C(x, x, "id"(x)) [x in A]$],
//   nary(5)[$"idpeel"(c, d) in C(a, b, c)$],
// )

#prooftree(
  axi[$a in A$],
  axi[$C(x,y,z) "set" [x ∈ A, y ∈ A, z ∈ "Id"(A,x,y)]$],
  axi[$d(x)∈ C(x,x,id(x)) [x∈A]$],
  tri[$"idpeel"(id(a), d) = d(a) ∈ C(a, a, id(a))$],
)

In our problem, $"trans"(id(a), d)$ exactly matches this format.
This means we can just macro-expand the left side of the definition:

$
  "trans"(id(a), d) &=_[a =_A b] d \
  "apply"("idpeel"(id(a), (x)lambda y.y), d) &=_[a =_A b] d \
  "apply"(((x)lambda y.y)(a), d) &=_[a =_A b] d \
  "apply"((lambda y.y), d) &=_[a =_A b] d \
  d &=_[a =_A b] d \
$

This means we're really looking for a definition for $"unitl"(a, d) in [d =_[a =_A b] d]$.
This can just be constructed using the canonical element $id(d)$. The full derivation looks like this:

#prooftree(
  axi[$A "set"$],
  axi[$a in A$],
  axi[$b in A$],
  axi[$d in [a =_A b]$],
  nary(4, right_label: "Reflexivity")[$d = d in [a =_A b]$],
)

#prooftree(
  axi[$A "set"$],
  axi[$a in A$],
  axi[$b in A$],
  axi[$d in [a =_A b]$],
  nary(4, right_label: "Id-introduction")[$id(d) in [d =_[a =_A b] d]$],
)