---

Step * 1 2 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}
8. (a ∨ b) = b ∈ {X ⊢ _:T}
⊢ (w @ 1(𝕀) ∨ (a ∨ b)) = b ∈ {X ⊢ _:T}
BY
{ (Fold `same-cubical-term` 0
   THEN (InstLemma `case-term-same2` [⌜X⌝;⌜psi⌝;⌜1(𝔽)⌝;⌜T⌝;⌜w @ 1(𝕀)⌝;⌜(a ∨ b)⌝;⌜b⌝]⋅ THENA Auto)
   ) }

1
.....antecedent..... 
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}
⊢ X, 1(𝔽) ⊢ (a ∨ b)=b: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}
9. X, (psi ∨ 1(𝔽)) ⊢ (w @ 1(𝕀) ∨ (a ∨ b))=b:T
⊢ X ⊢ (w @ 1(𝕀) ∨ (a ∨ b))=b: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
8.  (a  \mvee{}  b)  =  b
\mvdash{}  (w  @  1(\mBbbI{})  \mvee{}  (a  \mvee{}  b))  =  b


By

---

Latex:
(Fold  `same-cubical-term`  0
  THEN  (InstLemma  `case-term-same2`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}1(\mBbbF{})\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}w  @  1(\mBbbI{})\mkleeneclose{};\mkleeneopen{}(a  \mvee{}  b)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index