---

Step * 1 of Lemma truncation-property


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))
BY
{ (FunExt THEN Auto THEN BLemma `half-squash-equality` THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  Q  :  Type
3.  f  :  X  {}\mrightarrow{}  \00D9(Q)
4.  \mforall{}x:X.  ((|f|  |x|)  =  (f  x))
5.  g  :  \00D9(X)  {}\mrightarrow{}  \00D9(Q)
\mvdash{}  g  =  |f|


By

---

Latex:
(FunExt  THEN  Auto  THEN  BLemma  `half-squash-equality`  THEN  Auto)

---

Home Index