---

Step * of Lemma paths-are-refl-iff

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}].
  uiff(∀Z:j⊢. ∀s:Z j⟶ X. ∀p:{Z ⊢ _:Path((A)s)}.  (p = refl(p @ 0(𝕀)) ∈ {Z ⊢ _:Path((A)s)});∀Z:j⊢. ∀s:Z j⟶ X.
                                                                                            ∀p:{Z ⊢ _:Path((A)s)}.
                                                                                              ∀[x,y:{Z ⊢ _:𝕀}].
                                                                                                (p @ x
                                                                                                = p @ y
                                                                                                ∈ {Z ⊢ _:(A)s}))
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. ∀Z:j⊢. ∀s:Z j⟶ X. ∀p:{Z ⊢ _:Path((A)s)}.  (p = refl(p @ 0(𝕀)) ∈ {Z ⊢ _:Path((A)s)})
⊢ ∀Z:j⊢. ∀s:Z j⟶ X. ∀p:{Z ⊢ _:Path((A)s)}.  ∀[x,y:{Z ⊢ _:𝕀}].  (p @ x = p @ y ∈ {Z ⊢ _:(A)s})

2
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. ∀Z:j⊢. ∀s:Z j⟶ X. ∀p:{Z ⊢ _:Path((A)s)}.  ∀[x,y:{Z ⊢ _:𝕀}].  (p @ x = p @ y ∈ {Z ⊢ _:(A)s})
⊢ ∀Z:j⊢. ∀s:Z j⟶ X. ∀p:{Z ⊢ _:Path((A)s)}.  (p = refl(p @ 0(𝕀)) ∈ {Z ⊢ _:Path((A)s)})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].
    uiff(\mforall{}Z:j\mvdash{}.  \mforall{}s:Z  j{}\mrightarrow{}  X.  \mforall{}p:\{Z  \mvdash{}  \_:Path((A)s)\}.    (p  =  refl(p  @  0(\mBbbI{})));\mforall{}Z:j\mvdash{}.  \mforall{}s:Z  j{}\mrightarrow{}  X.
                                                                                                                                              \mforall{}p:\{Z  \mvdash{}  \_:Path((A)s)\}.
                                                                                                                                                  \mforall{}[x,y:\{Z  \mvdash{}  \_:\mBbbI{}\}].
                                                                                                                                                      (p  @  x  =  p  @  y))


By

---

Latex:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index