---

Step * of Lemma truncation-property

∀[X,Q:Type].  ∀f:X ⟶ ⇃(Q). ((∀x:X. ((|f| |x|) = (f x) ∈ ⇃(Q))) ∧ (∀g:⇃(X) ⟶ ⇃(Q). (g = |f| ∈ (⇃(X) ⟶ ⇃(Q)))))
BY
{ Auto }

1
1. X : Type
2. Q : Type
3. f : X ⟶ ⇃(Q)
4. ∀x:X. ((|f| |x|) = (f x) ∈ ⇃(Q))
5. g : ⇃(X) ⟶ ⇃(Q)
⊢ g = |f| ∈ (⇃(X) ⟶ ⇃(Q))

---

Latex:

---

Latex:
\mforall{}[X,Q:Type].    \mforall{}f:X  {}\mrightarrow{}  \00D9(Q).  ((\mforall{}x:X.  ((|f|  |x|)  =  (f  x)))  \mwedge{}  (\mforall{}g:\00D9(X)  {}\mrightarrow{}  \00D9(Q).  (g  =  |f|)))


By

---

Latex:
Auto

---

Home Index