---

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

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[pr:{X ⊢ _:Fiber(w;a)}]. ∀[cT:X +⊢ Compositon(T)].
∀[cA:X +⊢ Compositon(A)].
  (fiber-member(transprt-const(X;fiber-comp(X;T;A;w;a;cT;cA);pr)) = transprt-const(X;cT;pr.1) ∈ {X ⊢ _:T})
BY
{ (Intros
   THEN (Enough to prove app((w)p; q) ∈ {X.T ⊢ _:(A)p}
          Because (Unfolds ``fiber-member fiber-comp`` 0
                   THEN (InstLemma `fst-transprt-const-sigma` [⌜X⌝]⋅ THENA Auto)
                   THEN BHyp -1
                   THEN Auto))
   ) }

1
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}

---

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{}[pr:\{X  \mvdash{}  \_:Fiber(w;a)\}].
\mforall{}[cT:X  +\mvdash{}  Compositon(T)].  \mforall{}[cA:X  +\mvdash{}  Compositon(A)].
    (fiber-member(transprt-const(X;fiber-comp(X;T;A;w;a;cT;cA);pr))  =  transprt-const(X;cT;pr.1))


By

---

Latex:
(Intros
  THEN  (Enough  to  prove  app((w)p;  q)  \mmember{}  \{X.T  \mvdash{}  \_:(A)p\}
                Because  (Unfolds  ``fiber-member  fiber-comp``  0
                                  THEN  (InstLemma  `fst-transprt-const-sigma`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                  THEN  BHyp  -1
                                  THEN  Auto))
  )

---

Home Index