---

Step * 1 of Lemma cubical-fiber-id-fun

.....subterm..... T:t
4:n
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. u : {X ⊢ _:T}
⊢ app((cubical-id-fun(X))p; q) = q ∈ {X.T ⊢ _:(T)p}
BY
{ ((InstLemmaIJ `csm-cubical-id-fun` [⌜X⌝;⌜T⌝;⌜X.T⌝;⌜p⌝]⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜app(Z; q)⌝ ⌜{X.T ⊢ _:(T)p}⌝ (-1)⋅ THENA Auto)
   THEN NthHypEqGen (-1)
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
4:n
1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  u  :  \{X  \mvdash{}  \_:T\}
\mvdash{}  app((cubical-id-fun(X))p;  q)  =  q


By

---

Latex:
((InstLemmaIJ  `csm-cubical-id-fun`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X.T\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}app(Z;  q)\mkleeneclose{}  \mkleeneopen{}\{X.T  \mvdash{}  \_:(T)p\}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  NthHypEqGen  (-1)
  THEN  EqCDA
  THEN  Auto)

---

Home Index