---

Step * of Lemma paths-are-refl-iff2

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.𝕀 ⊢ _:((A)s)p}.
                                                                                              ∀[x,y:{Z ⊢ _:𝕀}].
                                                                                                ((p)[x]
                                                                                                = (p)[y]
                                                                                                ∈ {Z ⊢ _:(A)s}))
BY
{ (InstLemma `paths-are-refl-iff` []
   THEN RepeatFor 2 (ParallelLast')
   THEN ((D -1 THEN D 0) THEN (D 0 THENA Auto))
   THEN ThinTrivial
   THEN ((D -2 THENM Try (Trivial)) ORELSE Thin 3)
   THEN RepeatFor 2 (ParallelLast)) }

1
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})
4. Z : CubicalSet{j}
5. ∀s:Z j⟶ X. ∀p:{Z ⊢ _:Path((A)s)}.  ∀[x,y:{Z ⊢ _:𝕀}].  (p @ x = p @ y ∈ {Z ⊢ _:(A)s})
6. s : Z j⟶ X
7. ∀p:{Z ⊢ _:Path((A)s)}. ∀[x,y:{Z ⊢ _:𝕀}].  (p @ x = p @ y ∈ {Z ⊢ _:(A)s})
⊢ ∀p:{Z.𝕀 ⊢ _:((A)s)p}. ∀[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}) 
   supposing ∀Z:j⊢. ∀s:Z j⟶ X. ∀p:{Z ⊢ _:Path((A)s)}.  (p = refl(p @ 0(𝕀)) ∈ {Z ⊢ _:Path((A)s)})
4. ∀Z:j⊢. ∀s:Z j⟶ X. ∀p:{Z.𝕀 ⊢ _:((A)s)p}.  ∀[x,y:{Z ⊢ _:𝕀}].  ((p)[x] = (p)[y] ∈ {Z ⊢ _:(A)s})
5. Z : CubicalSet{j}
6. ∀s:Z j⟶ X. ∀p:{Z.𝕀 ⊢ _:((A)s)p}.  ∀[x,y:{Z ⊢ _:𝕀}].  ((p)[x] = (p)[y] ∈ {Z ⊢ _:(A)s})
7. s : Z j⟶ X
8. ∀p:{Z.𝕀 ⊢ _:((A)s)p}. ∀[x,y:{Z ⊢ _:𝕀}].  ((p)[x] = (p)[y] ∈ {Z ⊢ _:(A)s})
⊢ ∀p:{Z ⊢ _:Path((A)s)}. ∀[x,y:{Z ⊢ _:𝕀}].  (p @ x = p @ y ∈ {Z ⊢ _:(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.\mBbbI{}  \mvdash{}  \_:((A)s)p\}.
                                                                                                                                                  \mforall{}[x,y:\{Z  \mvdash{}  \_:\mBbbI{}\}].
                                                                                                                                                      ((p)[x]  =  (p)[y]))


By

---

Latex:
(InstLemma  `paths-are-refl-iff`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  ((D  -1  THEN  D  0)  THEN  (D  0  THENA  Auto))
  THEN  ThinTrivial
  THEN  ((D  -2  THENM  Try  (Trivial))  ORELSE  Thin  3)
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index