---

Step * 1 of Lemma cubical-fiber_wf


1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
⊢ app((w)p; q) ∈ {X.T ⊢ _:(A)p}
BY
{ ((Assert q ∈ {X.T ⊢ _:(T)p} BY
          Auto)
   THEN (Assert (w)p ∈ {X.T ⊢ _:((T ⟶ A))p} BY
               Auto)
   THEN (InstLemma `csm-cubical-fun` [⌜parm{i|j}⌝; ⌜parm{i}⌝;⌜X⌝;X.T;⌜T⌝;⌜A⌝;⌜p⌝]⋅ THENA Auto)
   THEN (Assert (w)p ∈ {X.T ⊢ _:((T)p ⟶ (A)p)} BY
               (InferEqualTypeUp THEN Auto))) }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. q ∈ {X.T ⊢ _:(T)p}
7. (w)p ∈ {X.T ⊢ _:((T ⟶ A))p}
8. ((T ⟶ A))p = (X.T ⊢ (T)p ⟶ (A)p) ∈ {X.T ⊢ _}
9. (w)p ∈ {X.T ⊢ _:((T)p ⟶ (A)p)}
⊢ app((w)p; q) ∈ {X.T ⊢ _:(A)p}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  A  :  \{X  \mvdash{}  \_\}
4.  w  :  \{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
5.  a  :  \{X  \mvdash{}  \_:A\}
\mvdash{}  app((w)p;  q)  \mmember{}  \{X.T  \mvdash{}  \_:(A)p\}


By

---

Latex:
((Assert  q  \mmember{}  \{X.T  \mvdash{}  \_:(T)p\}  BY
                Auto)
  THEN  (Assert  (w)p  \mmember{}  \{X.T  \mvdash{}  \_:((T  {}\mrightarrow{}  A))p\}  BY
                          Auto)
  THEN  (InstLemma  `csm-cubical-fun`  [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};  \mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};X.T;\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (w)p  \mmember{}  \{X.T  \mvdash{}  \_:((T)p  {}\mrightarrow{}  (A)p)\}  BY
                          (InferEqualTypeUp  THEN  Auto)))

---

Home Index