67 lines
1.6 KiB
Plaintext
67 lines
1.6 KiB
Plaintext
#set document(title: "Homework 2", author: "Michael Zhang <zhan4854@umn.edu>")
|
||
#set page("us-letter")
|
||
#import "@preview/prooftrees:0.1.0": *
|
||
#import emoji: face
|
||
#let prooftree(..args) = tree(
|
||
tree_config: tree_config(
|
||
vertical_spacing: 6pt,
|
||
),
|
||
..args
|
||
)
|
||
|
||
= Homework 2
|
||
|
||
Michael Zhang \<zhan4854\@umn.edu\>
|
||
|
||
#let c(body) = {
|
||
set text(gray)
|
||
body
|
||
}
|
||
#let subst = $"subst"$
|
||
#let tt = $"tt"$
|
||
|
||
#c[Assume you have $"Id"$ and $"U"$ but not $"Eq"$ (or $hat("Eq")$). Write down an abstraction $p$ such that
|
||
|
||
#prooftree(
|
||
axi[$a in A [Gamma]$],
|
||
axi[$b in B [Gamma]$],
|
||
bin[$p(a, b) in "Id"(A+B, "inl"(a), "inr"(b)) arrow.r emptyset [Gamma]$]
|
||
)
|
||
|
||
is derivable. You do not have to prove in your submission that it is derivable.]
|
||
|
||
Wait isn't this just the same as the Peano's fourth axiom as given in the book?
|
||
|
||
$
|
||
p(a, b) &equiv lambda ((x) subst(x, tt)) \
|
||
$
|
||
|
||
where
|
||
|
||
- $subst(c, p) equiv "apply"("idpeel"(c, (x) lambda x.x), p)$
|
||
|
||
#prooftree(
|
||
axi[$A "set"$],
|
||
axi[$B "set"$],
|
||
bin[$A + B "set"$],
|
||
axi[$a in A$],
|
||
axi[$b in B$],
|
||
axi[$p in "Id"(A + B, "inl"(a), "inr"(b))$],
|
||
axi[$P(x) "set" [x in A + B]$],
|
||
nary(5)[$subst(p, "inl"(a)) equiv "apply"("idpeel"(p, (g) lambda y.y), "inl"(a)) in P("inr"(b))$],
|
||
)
|
||
|
||
- $P(m) equiv "Set"("when"(m, (x)hat(top), (y)hat({})))$
|
||
|
||
// (Agda implementation #face.smile.slight)
|
||
|
||
// ```agda
|
||
// discriminate : {A : Set} {B : Set} → (s : A ⊎ B) → Set
|
||
// discriminate (inj₁ x) = ⊤
|
||
// discriminate (inj₂ y) = ⊥
|
||
|
||
// problem2 : {A : Set} {B : Set}
|
||
// → (a : A) → (b : B)
|
||
// → inj₁ a ≢ inj₂ b
|
||
// problem2 a b p = subst discriminate p tt
|
||
// ``` |