---

Step * of Lemma paths-equal

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[p:{X ⊢ _:(Path_A a b)}]. ∀[q:{X ⊢ _:Path(A)}].
  p = q ∈ {X ⊢ _:(Path_A a b)} supposing p = q ∈ {X ⊢ _:Path(A)}
BY
{ (Intros
   THEN SubsumeC ⌜{t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = a ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = b ∈ {X ⊢ _:A})} ⌝⋅
   THEN Try ((EqTypeCD THEN Auto))) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. p : {X ⊢ _:(Path_A a b)}
6. q : {X ⊢ _:Path(A)}
7. p = q ∈ {X ⊢ _:Path(A)}
⊢ p @ 0(𝕀) = a ∈ {X ⊢ _:A}

2
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. p : {X ⊢ _:(Path_A a b)}
6. q : {X ⊢ _:Path(A)}
7. p = q ∈ {X ⊢ _:Path(A)}
8. p @ 0(𝕀) = a ∈ {X ⊢ _:A}
⊢ p @ 1(𝕀) = b ∈ {X ⊢ _:A}

3
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. p : {X ⊢ _:(Path_A a b)}
6. q : {X ⊢ _:Path(A)}
7. p = q ∈ {X ⊢ _:Path(A)}
8. p = q ∈ {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = a ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = b ∈ {X ⊢ _:A})} 
⊢ {t:{X ⊢ _:Path(A)}| (t @ 0(𝕀) = a ∈ {X ⊢ _:A}) ∧ (t @ 1(𝕀) = b ∈ {X ⊢ _:A})}  ⊆r {X ⊢ _:(Path_A a b)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[p:\{X  \mvdash{}  \_:(Path\_A  a  b)\}].  \mforall{}[q:\{X  \mvdash{}  \_:Path(A)\}].
    p  =  q  supposing  p  =  q


By

---

Latex:
(Intros
  THEN  SubsumeC  \mkleeneopen{}\{t:\{X  \mvdash{}  \_:Path(A)\}|  (t  @  0(\mBbbI{})  =  a)  \mwedge{}  (t  @  1(\mBbbI{})  =  b)\}  \mkleeneclose{}\mcdot{}
  THEN  Try  ((EqTypeCD  THEN  Auto)))

---

Home Index