---

Step * 1 1 of Lemma free-group-adjunction


1. d : Type
⊢ fg-lift(free-group(free-word(d));λx.free-letter(free-letter(x))) ∈ MonHom(free-group(d),free-group(free-word(d)))
BY
{ (InstLemma `fg-lift_wf` [⌜d⌝;⌜free-group(free-word(d))⌝;⌜λx.free-letter(free-letter(x))⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  d  :  Type
\mvdash{}  fg-lift(free-group(free-word(d));\mlambda{}x.free-letter(free-letter(x)))
    \mmember{}  MonHom(free-group(d),free-group(free-word(d)))


By

---

Latex:
(InstLemma  `fg-lift\_wf`  [\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}free-group(free-word(d))\mkleeneclose{};\mkleeneopen{}\mlambda{}x.free-letter(free-letter(x))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index