---

Step * of Lemma h-level_wf

No Annotations
∀[n:ℕ]. ∀[X:j⊢]. ∀[A:{X ⊢ _}].  X ⊢ h-level(X;n;A)
BY
{ (InductionOnNat
   THEN Unfold `h-level` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN Try (Fold `h-level` 0)) }

1
1. n : ℤ
⊢ ∀[X:j⊢]. ∀[A:{X ⊢ _}].  X ⊢ Contractible(A)

2
1. n : ℤ
2. 0 < n
3. ∀[X:j⊢]. ∀[A:{X ⊢ _}].  X ⊢ h-level(X;n - 1;A)
⊢ ∀[X:j⊢]. ∀[A:{X ⊢ _}].
    X ⊢ if n <z 1 then λA.Contractible(A) else λA.h-level(X;n - 1;ΠA Π(A)p (Path_((A)p)p (q)p q)) fi  A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].    X  \mvdash{}  h-level(X;n;A)


By

---

Latex:
(InductionOnNat
  THEN  Unfold  `h-level`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Fold  `h-level`  0))

---

Home Index