---

Step * 1 of Lemma fiber-point_wf

.....implicit subterm..... 
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. t : {X ⊢ _:T}
7. c : {X ⊢ _:(Path_A a app(f; t))}
⊢ X.T ⊢ (Path_(A)p (a)p app((f)p; q))
BY
{ Auto }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. f : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. t : {X ⊢ _:T}
7. c : {X ⊢ _:(Path_A a app(f; t))}
⊢ app((f)p; q) ∈ {X.T ⊢ _:(A)p}

---

Latex:

---

Latex:
.....implicit  subterm..... 
1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  A  :  \{X  \mvdash{}  \_\}
4.  f  :  \{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
5.  a  :  \{X  \mvdash{}  \_:A\}
6.  t  :  \{X  \mvdash{}  \_:T\}
7.  c  :  \{X  \mvdash{}  \_:(Path\_A  a  app(f;  t))\}
\mvdash{}  X.T  \mvdash{}  (Path\_(A)p  (a)p  app((f)p;  q))


By

---

Latex:
Auto

---

Home Index