45 lines
1.1 KiB
Text
45 lines
1.1 KiB
Text
|
#set document(title: "Homework 2", author: "Michael Zhang <zhan4854@umn.edu>")
|
|||
|
|
#set page("us-letter")
|
|||
|
|
#import "@preview/prooftrees:0.1.0": *
|
|||
|
|
#import emoji: face
|
|||
|
|
|
|||
|
|
= Homework 2
|
|||
|
|
|
|||
|
|
Michael Zhang \<zhan4854\@umn.edu\>
|
|||
|
|
|
|||
|
|
#let c(body) = {
|
|||
|
|
set text(gray)
|
|||
|
|
body
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
#c[Assume you have $"Id"$ and $"U"$ but not $"Eq"$ (or $hat("Eq")$). Write down an abstraction $p$ such that
|
|||
|
|
|
|||
|
|
#tree(
|
|||
|
|
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
|
|||
|
|
- $P(m) = "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
|
|||
|
|
// ```
|