---

Step * of Lemma fiber-comp_wf

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[w:{X ⊢ _:(T ⟶ A)}]. ∀[a:{X ⊢ _:A}]. ∀[cT:X ⊢ Compositon(T)]. ∀[cA:X +⊢ Compositon(A)].
  (fiber-comp(X;T;A;w;a;cT;cA) ∈ X ⊢ Compositon(Fiber(w;a)))
BY
{ ((Auto
    THEN (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 Unfolds ``cubical-fiber`` 0
   THEN ProveWfLemma) }

---

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


By

---

Latex:
((Auto
    THEN  (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  Unfolds  ``cubical-fiber``  0
  THEN  ProveWfLemma)

---

Home Index