#set page("us-letter")

#let natrec = text[natrec]
#let suc = text[suc]

#let c(body) = {
  set text(gray)
  body
}

Define `funsplit` in terms of `apply`.

#c[Define `funsplit` in terms of `apply`.]

NOTE: Is it "cheating" in some sense, to use the identity abstraction $(x) x$ in the place of the last parameter to $"apply"$?

Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:

#c[Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:

Please be pedantic and explicitly use a rule even for "obvious" steps. You do not have to draw a big derivation tree (which is difficult to typeset), but it should be clear which rule you are using at each step. If you are using an implicit rule that the authors did not explicitly write out, make it clear what it is. If you are not sure what a derivation tree is, whether a particular rule is allowed, or which emoji was just introduced in Emoji 15.1, use the Discord forum immediately.]
#set math.equation(numbering: "(1)")
First, let me reprint some rules from the textbook here to refer to them more easily from here on:
- Reflexivity (pg. 37 in textbook)
  $ #tree(axi[$a in A$], uni[$a = a in A$]) $
- Propositions as sets (pg. 37 in textbook)
  $ #tree(axi[$a∈A$], uni[$A "true"$]) $
- Substitution in elements from chapter 5 (pg. 38 in textbook)

Please be pedantic and explicitly use a rule even for "obvious" steps. You do not have to draw a big derivation tree (which is difficult to typeset), but it should be clear which rule you are using at each step. If you are using an implicit rule that the authors did not explicitly write out, make it clear what it is. If you are not sure what a derivation tree is, whether a particular rule is allowed, or which emoji was just introduced in Emoji 15.1, use the Discord forum immediately.

  $ #tree(
    axi[$c(x) in C(x) [x in A]$],
    axi[$a = b in A$],
    bin[$c(a) = c(b) in C(a)$],
  ) $
- Eq-introduction rule (pg. 60 in textbook)
  $ #tree(axi[$a = b in A$], uni[$"eq" in "Eq"(A, a, b)$]) $
- Strong Eq-elimination (pg. 61 in textbook)
  $ #tree(axi[$c ∈ "Eq"(A, a, b)$], uni[$a=b∈A$]) $
- N-introduction (pg. 63 in textbook)
  $ #tree(axi[$a in NN$], uni[$"suc"(a) in NN$]) $
- Nat rec (pg. 64 in textbook)
  $ #tree(
    axi[$a in NN$],
    axi[$C(v) "set" [v in NN]$],
    axi[$d in C(0)$],
    axi[$e(x, y) in C("suc"(x)) [x in NN, y in C(x)]$],
    nary(4)[$"natrec"(a, d, e) in C(a)$],
  ) $
- Peano's 5th axiom (pg. 65 in textbook)
  $ #tree(
    axi[$a ∈ NN$],
    axi[$C(v) "prop" [v ∈ N]$],
    axi[$C(0) "true"$],
    axi[$C("suc"(x)) "true" [C(x) "true"]$],
    nary(4)[$C(a) "true"$]
  ) $
I can now form the derivation:
$ #tree(
  axi[$0 in NN$],
  uni(right_label: "(1)")[$0 = 0 in NN$],
  uni(right_label: "natrec")[$"natrec"(0, 0, (u, v) "suc"(v)) = 0 in NN$],
  uni(right_label: "(4)")[$"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$],
) $
$ #tree(
  axi[$x = y in NN [x in NN, y in NN]$],
  uni(right_label: "(3, 6)")[$"suc"(x) = "suc"(y) in NN [x in NN, y in NN]$],
) $
  
$ #tree(
  axi(pad(bottom: .2em, [
    $x in NN$ \
    $"Eq"(NN, "natrec"(n, 0, (u, v) "suc"(v)), n) "set" [n in NN]$ \
    $"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$ \
    $"eq"_"suc" (x, y) in "Eq"(NN, "natrec"("suc"(x), 0, (u, v) "suc"(v)), "suc"(x)) [x in NN, y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)]$ \
  ])),
  uni[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
) $
#tree(
  axi[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
  uni(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
  uni(right_label: [#sym.plus.circle])[$plus.circle(x, 0) = x in NN [x in NN]$],
)
#pagebreak()
Then, we can use this:
#set math.equation(numbering: none)
#tree(
  axi[$0 in NN$],
  uni(right_label: "(1)")[$0 = 0 in NN$],
  uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$],
)
Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence:
#tree(
  axi[$"suc"(x) in C(x) [x in NN]$],
  axi[$x = y in NN$],
  bin[$"suc"(x) = "suc"(y) in NN$],
)
Then, convert this to Eq:
#tree(
  axi[$"suc"(x) = "suc"(y) in NN$],
  axi[$x = y in NN$],
  bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$],
)
We can form a lambda term over eq objects using $lambda$-introduction:
#tree(
  axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$],
  uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$],
)
This gives us what we need to perform induction over nats:
#tree(
  axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$],
  uni[]
)
#tree(
  axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$],
  uni[],
)
#tree(
  axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
  uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
  uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$],
)

---
#pagebreak()

    tree(
        axi[$C(v) "set" [v in NN]$],
        axi[$x in NN$],
        axi[$d in C(0)$],
        axi[$x in NN$],
        nary(4)[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],
    )

  let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]
  tree(
    axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$],
    uni[$split1 equiv x in NN [x in NN]$],
  )
  tree(
    // axi[$c in "Eq"(NN, split1, 0), x)$],
    axi[$split1 equiv x in NN [x in NN]$],
    uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
  )
  tree(
    axi[$c in "Eq"(NN, plus.circle(x, 0), x)$],
    uni[$plus.circle(x, 0) equiv x in NN [x in NN]$],
  )
  tree(
    axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
  )

    tree(
        axi[],
        uni[$plus.circle(x, 0) equiv natrec(x, 0, (u, v) suc(v)) [Gamma tack.r x in NN]$],
        axi[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],
        bin[$plus.circle(x, 0) equiv x in NN [(Gamma, Delta) tack.r x in NN]$],
    )

  tree(
    axi[$split1 equiv x [x in NN]$],
  )
  tree(
    axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
    axi[$split1 equiv x [x in NN]$],
    bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
  )

module hwk1 where
open import Data.Nat
open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning
natrec : {C : Set} → (a : ℕ) → (d : C) → (e : ℕ → C → C) → C
natrec zero d e = d
natrec (suc b) d e = e b (natrec b d e)
⊕ : ℕ → ℕ → ℕ
⊕ x y = natrec x y (λ u v → suc v)
problem2-lemma : (x : ℕ) → natrec x 0 (λ u v → suc v) ≡ x
problem2-lemma zero = refl
problem2-lemma (suc x) = cong suc (problem2-lemma x)
-- (λ u v → suc v) x (natrec x 0 (λ u v → suc v))
-- suc (natrec x 0 (λ u v → suc v))
 
problem2 : (x : ℕ) → ⊕ x 0 ≡ x
problem2 x = problem2-lemma x
--   begin
--     ⊕ x 0
--   ≡⟨⟩
--     natrec x 0 (λ u v → suc v)
--   ≡⟨ {!   !} ⟩
--     x
--   ∎

include: bidir

include: . bidir

_build