2023-11-06 04:02:07 +00:00
|
|
|
|
#set document(title: "Homework 2", author: "Michael Zhang <zhan4854@umn.edu>")
|
|
|
|
|
|
#set page("us-letter")
|
|
|
|
|
|
#import "@preview/prooftrees:0.1.0": *
|
|
|
|
|
|
#import emoji: face
|
2023-11-13 08:52:32 +00:00
|
|
|
|
#let prooftree(..args) = tree(
|
|
|
|
|
|
tree_config: tree_config(
|
|
|
|
|
|
vertical_spacing: 6pt,
|
|
|
|
|
|
),
|
|
|
|
|
|
..args
|
|
|
|
|
|
)
|
2023-11-06 04:02:07 +00:00
|
|
|
|
|
|
|
|
|
|
= Homework 2
|
|
|
|
|
|
|
|
|
|
|
|
Michael Zhang \<zhan4854\@umn.edu\>
|
|
|
|
|
|
|
|
|
|
|
|
#let c(body) = {
|
|
|
|
|
|
set text(gray)
|
|
|
|
|
|
body
|
|
|
|
|
|
}
|
2023-11-13 08:52:32 +00:00
|
|
|
|
#let subst = $"subst"$
|
|
|
|
|
|
#let tt = $"tt"$
|
2023-11-06 04:02:07 +00:00
|
|
|
|
|
|
|
|
|
|
#c[Assume you have $"Id"$ and $"U"$ but not $"Eq"$ (or $hat("Eq")$). Write down an abstraction $p$ such that
|
|
|
|
|
|
|
2023-11-13 08:52:32 +00:00
|
|
|
|
#prooftree(
|
2023-11-06 04:02:07 +00:00
|
|
|
|
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?
|
|
|
|
|
|
|
|
|
|
|
|
$
|
2023-11-13 08:52:32 +00:00
|
|
|
|
p(a, b) &equiv lambda ((x) subst(x, tt)) \
|
2023-11-06 04:02:07 +00:00
|
|
|
|
$
|
|
|
|
|
|
|
|
|
|
|
|
where
|
2023-11-13 08:52:32 +00:00
|
|
|
|
|
|
|
|
|
|
- $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({})))$
|
2023-11-06 04:02:07 +00:00
|
|
|
|
|
|
|
|
|
|
// (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
|
|
|
|
|
|
// ```
|
