wip

extra-problem-3.typ

@@ -0,0 +1,69 @@
+#import "@preview/prooftrees:0.1.0": *
+#show math.eq: math.scripts
+#let prooftree(..args) = tree(
+  tree_config: tree_config(
+    vertical_spacing: 6pt,
+  ),
+  ..args
+)
+
+= Problem 3
+
+Assume that you have Id but not Eq at your disposal, and you can only use rules. Write down an abstraction unitl ("unitl" for "unit left") such that:
+
+#prooftree(
+  axi[$ d ∈ [a =_A b] $],
+  uni[$ "unitl"(a, d) ∈ ["trans"(id(a), d) =_[a =_A b] d] $],
+)
+
+There's a trick here that you may notice if you remember the definition of "trans" and the computation rule for "idpeel":
+
+$
+  "trans"(d,e) ≡ "apply"("idpeel"(d,(x)lambda y.y),e)
+$
+
+// #tree(
+//   axi[$a in A$],
+//   axi[$b in A$],
+//   axi[$c in "Id"(A, a, b)$],
+//   axi[$C(x, y, z) "set" [x in A, y in A, z in "Id"(A, x, y)]$],
+//   axi[$d(x) in C(x, x, "id"(x)) [x in A]$],
+//   nary(5)[$"idpeel"(c, d) in C(a, b, c)$],
+// )
+
+#prooftree(
+  axi[$a in A$],
+  axi[$C(x,y,z) "set" [x ∈ A, y ∈ A, z ∈ "Id"(A,x,y)]$],
+  axi[$d(x)∈ C(x,x,id(x)) [x∈A]$],
+  tri[$"idpeel"(id(a), d) = d(a) ∈ C(a, a, id(a))$],
+)
+
+In our problem, $"trans"(id(a), d)$ exactly matches this format.
+This means we can just macro-expand the left side of the definition:
+
+$
+  "trans"(id(a), d) &=_[a =_A b] d \
+  "apply"("idpeel"(id(a), (x)lambda y.y), d) &=_[a =_A b] d \
+  "apply"(((x)lambda y.y)(a), d) &=_[a =_A b] d \
+  "apply"((lambda y.y), d) &=_[a =_A b] d \
+  d &=_[a =_A b] d \
+$
+
+This means we're really looking for a definition for $"unitl"(a, d) in [d =_[a =_A b] d]$.
+This can just be constructed using the canonical element $id(d)$. The full derivation looks like this:
+
+#prooftree(
+  axi[$A "set"$],
+  axi[$a in A$],
+  axi[$b in A$],
+  axi[$d in [a =_A b]$],
+  nary(4, right_label: "Reflexivity")[$d = d in [a =_A b]$],
+)
+
+#prooftree(
+  axi[$A "set"$],
+  axi[$a in A$],
+  axi[$b in A$],
+  axi[$d in [a =_A b]$],
+  nary(4, right_label: "Id-introduction")[$id(d) in [d =_[a =_A b] d]$],
+)

extraexercises.agda

@@ -10,22 +10,56 @@ J : {A : Set}
   → (x y : A) → (p : x ≡ y) → C x y p
 J C c x x refl = c x
 
+-- Translation to PMLTT concepts
+
+id : {A : Set} (a : A) → a ≡ a
+id a = refl
+
+idpeel : {A : Set} {a b : A}
+  → (c : a ≡ b)
+  → {C : (x y : A) → (z : x ≡ y) → Set}
+  → (d : (x : A) → C x x (id x))
+  → C a b c
+idpeel {A} {a} {b} c {C} d = J C d a b c
+
+-- Problem 2
+
 inv : {A : Set} {a b : A}
   → (d : a ≡ b)
   → sym (sym d) ≡ d
 inv {A} {a} {b} d = 
-    J (λ x y p → sym (sym p) ≡ p  ) (λ x → refl) a b d
+    J (λ x y p → sym (sym p) ≡ p) (λ x → refl) a b d
 
--- Problem 2
+-- assoc : {A : Set} {a b c d : A}
+--   → (e : a ≡ b)
+--   → (f : b ≡ c)
+--   → (g : c ≡ d)
+--   → trans (trans e f) g ≡ trans e (trans f g)
+-- assoc {a} {b} {c} {d} e f g =
+--   let whatever = (λ f → J (λ x y p → trans (trans x f) y ≡ trans x (trans f y)) (λ x → {! !}) {!   !} {!   !} {!   !}) in
+--   {!   !}
 
-assoc : {A : Set} {a b c d : A}
-  → (e : a ≡ b)
-  → (f : b ≡ c)
-  → (g : c ≡ d)
-  → trans (trans e f) g ≡ trans e (trans f g)
-assoc {a} {b} {c} {d} e f g =
-  let whatever = J {!   !} {!   !} {!   !} {!   !} {!   !} in
-  {!   !}
+-- Problem 3
+
+unitl : {A : Set}
+  → (a : A)
+  → {b : A}
+  → (d : a ≡ b)
+  → trans (id a) d ≡ d
+unitl a d = id d
+
+-- Problem 4
+
+unitr : {A : Set}
+  → {a : A}
+  → (b : A)
+  → (d : a ≡ b)
+  → trans d (id b) ≡ d
+unitr {A} {a} b d = J (λ x y p → trans p (id y) ≡ p) (λ x → id (id x)) a b d
+
+-- Problem 5
+
+-- ap : {A : Set}
 
 -- Problem 6
 

hwk1.typ

@@ -94,8 +94,10 @@ First, let me reprint some rules from the textbook here to refer to them more ea
 I can now form the derivation:
 
 $ #tree(
+  axi[],
+  uni[$NN "set"$],
   axi[$0 in NN$],
-  uni(right_label: "(1)")[$0 = 0 in NN$],
+  bin(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)$],
 ) $
@@ -119,8 +121,9 @@ $ #pad(left: -4em, tree(
 )) $
 
 #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, 11)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
+  axi[],
+  uni(right_label: "(11)")[$"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]$],
 )
 

hwk2.agda

@@ -0,0 +1,30 @@
+module hwk2 where
+
+open import Data.Nat
+open import Data.Sum
+open import Data.Unit
+open import Data.Empty
+open import Relation.Binary.PropositionalEquality as Eq hiding (subst)
+open Eq.≡-Reasoning
+
+J : {A : Set}
+  → (C : (x y : A) → x ≡ y → Set)
+  → (c : (x : A) → C x x refl)
+  → (x y : A) → (p : x ≡ y) → C x y p
+J C c x x refl = c x
+
+subst : {A : Set} {a b : A}
+  → (P : A → Set) 
+  → (c : a ≡ b)
+  → (p : P a)
+  → P b
+subst {A} {a} {b} P c = J (λ x y p → (P x → P y)) (λ x → (λ a → a)) a b c
+
+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

hwk2.typ

@@ -0,0 +1,45 @@
+#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
+// ```

scratch.typ

@@ -0,0 +1,74 @@
+#import "@preview/prooftrees:0.1.0": *
+
+= 1
+
+#tree(
+  axi[$d in [a =_A b]$],
+  uni[$"inv"(d) in ["symm"("symm"(d)) =_[a =_A b] d]$],
+)
+
+Defined by:
+
+$
+  "inv"(d) equiv "idpeel"(d, (x) id(id(x)))
+$
+
+Derivation tree:
+
+#tree(
+  axi[],
+  uni[$A "set"$],
+)
+
+= 2
+
+```
+d∈[a=A b] e∈[b=A c]
+-------------------
+     trans(d, e) ∈ [a =A c]
+
+trans(d,e) ≡ apply(idpeel(d,(x)λy.y),e)
+```
+
+```
+trans (trans e f) g == trans e (trans f g)
+
+apply(idpeel(
+  apply(idpeel(e, (x)\y.y), f),
+  (x)\y.y,
+), g)
+```
+
+= 3
+
+#tree(
+  axi[$d in [a =_A b]$],
+  uni[$"unitl"(a, d) ∈ ["trans"(id(a), d) =_[a =_A b] d]$]
+)
+
+---
+
+Simplifying the output type:
+
+$
+  "trans"(id(a), d) &=_[a =_A b] d \
+  "apply"("idpeel"(id(a), (x)lambda y.y), d) &=_[a =_A b] d \
+  "apply"(((x)lambda y.y)(a), d) &=_[a =_A b] d \
+  "apply"((lambda y.y), d) &=_[a =_A b] d \
+  d &=_[a =_A b] d \
+$
+
+This is just a reflexive equality so can be satisfied by $"id"$:
+
+$ "unitl"(a, d) equiv id(d) $
+
+= 4
+
+#tree(
+  axi[$d in [a =_A b]$],
+  uni[$"unitr"(d, b) in ["trans"(d, id(b)) =_[a =_A b] d]$],
+)
+
+$
+  "unitr"(d, b) equiv "idpeel"(d, (x)id(id(x))) \
+$