---

Step * of Lemma path-type-ext-eq

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}].
  {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = a ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = b ∈ {X ⊢ _:A})}  ≡ {X ⊢ _:(Path_A a b)}
BY
{ (Auto THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. x : {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = a ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = b ∈ {X ⊢ _:A})} 
⊢ x ∈ {X ⊢ _:(Path_A a b)}

2
.....subterm..... T:t
1:n
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. x : {X ⊢ _:(Path_A a b)}
⊢ x ∈ {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = a ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = b ∈ {X ⊢ _:A})} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].
    \{t:\{X  \mvdash{}  \_:Path(A)\}|  (t  @  0(\mBbbI{})  =  a)  \mwedge{}  (t  @  1(\mBbbI{})  =  b)\}    \mequiv{}  \{X  \mvdash{}  \_:(Path\_A  a  b)\}


By

---

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

---

Home Index