---

Step * 1 of Lemma fiber-member-transprt-const-fiber-comp


1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. pr : {X ⊢ _:Fiber(w;a)}
7. cT : X +⊢ Compositon(T)
8. cA : X +⊢ Compositon(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 (InstLemmaIJ `csm-cubical-fun` [⌜X⌝;X.T;⌜T⌝;⌜A⌝;⌜p⌝]⋅ THENA Auto)
   THEN (Assert (w)p ∈ {X.T ⊢ _:((T)p ⟶ (A)p)} BY
               (InferEqualType THEN Auto))
   THEN BLemma `cubical-app_wf_fun` 
   THEN Auto) }

---

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\}
6.  pr  :  \{X  \mvdash{}  \_:Fiber(w;a)\}
7.  cT  :  X  +\mvdash{}  Compositon(T)
8.  cA  :  X  +\mvdash{}  Compositon(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  (InstLemmaIJ  `csm-cubical-fun`  [\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
                          (InferEqualType  THEN  Auto))
  THEN  BLemma  `cubical-app\_wf\_fun` 
  THEN  Auto)

---

Home Index