---

Step * of Lemma csm-fiber-member

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[p:{X ⊢ _:Fiber(w;a)}]. ∀[H:j⊢]. ∀[s:H j⟶ X].
  ((fiber-member(p))s = fiber-member((p)s) ∈ {H ⊢ _:(T)s})
BY
{ (Intros
   THEN Unhide
   THEN Unfold `cubical-fiber` -3
   THEN Unfold `fiber-member` 0
   THEN (InstLemma `csm-ap-cubical-fst` [⌜X⌝;⌜H⌝;⌜T⌝]⋅ THENA Auto)
   THEN BHyp -1
   THEN Try (Trivial)) }

1
.....wf..... 
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. A : {X ⊢ _}
4. w : {X ⊢ _:(T ⟶ A)}
5. a : {X ⊢ _:A}
6. p : {X ⊢ _:Σ T (Path_(A)p (a)p app((w)p; q))}
7. H : CubicalSet{j}
8. s : H j⟶ X
9. ∀[B:{X.T ⊢ _}]. ∀[p:{X ⊢ _:Σ T B}]. ∀[s:H j⟶ X].  ((p.1)s = (p)s.1 ∈ {H ⊢ _:(T)s})
⊢ X.T ⊢ (Path_(A)p (a)p app((w)p; q))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[w:\{X  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[p:\{X  \mvdash{}  \_:Fiber(w;a)\}].  \mforall{}[H:j\mvdash{}].
\mforall{}[s:H  j{}\mrightarrow{}  X].
    ((fiber-member(p))s  =  fiber-member((p)s))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `cubical-fiber`  -3
  THEN  Unfold  `fiber-member`  0
  THEN  (InstLemma  `csm-ap-cubical-fst`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1
  THEN  Try  (Trivial))

---

Home Index