---

Step * 1 of Lemma path-term-1


1. X : CubicalSet{j}
2. psi : {X ⊢ _:𝔽}
3. T : {X ⊢ _}
4. a : {X ⊢ _:T}
5. b : {X ⊢ _:T}
6. w : {X, psi ⊢ _:(Path_T a b)}
7. w @ 1(𝕀) = b ∈ {X, psi ⊢ _:T}
⊢ (w @ 1(𝕀) ∨ (a ∨ b)) = b ∈ {X ⊢ _:T}
BY
{ Assert ⌜(a ∨ b) = b ∈ {X ⊢ _:T}⌝⋅ }

1
.....assertion..... 
1. X : CubicalSet{j}
2. psi : {X ⊢ _:𝔽}
3. T : {X ⊢ _}
4. a : {X ⊢ _:T}
5. b : {X ⊢ _:T}
6. w : {X, psi ⊢ _:(Path_T a b)}
7. w @ 1(𝕀) = b ∈ {X, psi ⊢ _:T}
⊢ (a ∨ b) = b ∈ {X ⊢ _:T}

2
1. X : CubicalSet{j}
2. psi : {X ⊢ _:𝔽}
3. T : {X ⊢ _}
4. a : {X ⊢ _:T}
5. b : {X ⊢ _:T}
6. w : {X, psi ⊢ _:(Path_T a b)}
7. w @ 1(𝕀) = b ∈ {X, psi ⊢ _:T}
8. (a ∨ b) = b ∈ {X ⊢ _:T}
⊢ (w @ 1(𝕀) ∨ (a ∨ b)) = b ∈ {X ⊢ _:T}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  psi  :  \{X  \mvdash{}  \_:\mBbbF{}\}
3.  T  :  \{X  \mvdash{}  \_\}
4.  a  :  \{X  \mvdash{}  \_:T\}
5.  b  :  \{X  \mvdash{}  \_:T\}
6.  w  :  \{X,  psi  \mvdash{}  \_:(Path\_T  a  b)\}
7.  w  @  1(\mBbbI{})  =  b
\mvdash{}  (w  @  1(\mBbbI{})  \mvee{}  (a  \mvee{}  b))  =  b


By

---

Latex:
Assert  \mkleeneopen{}(a  \mvee{}  b)  =  b\mkleeneclose{}\mcdot{}

---

Home Index