69 lines
1.9 KiB
Text
69 lines
1.9 KiB
Text
|
#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]$],
|
||
|
|
)
|