#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
// ```